I wanted to verify the validity of my proof for the property of derivation operator for formal context. I will not go to detail that much and simply define few things before indroducing the property that is of interest.
$\Bbb{K}=(G,M,I)$ is formal context where $G$ and $M$ are sets of objects and attributes, respectively, and $I$ is a binary relation from $G$ to $M$. Derivation operator (in some literatures, it is also known as concept-forming operator), denoted as $(\cdot^{'})$, is given below. $$ A^{'} = \{m\in M|gIm:\forall g\in A\}, \\ B^{'} = \{g\in G|gIm:\forall m\in B\} $$ where $A \subseteq G$ and $B \subseteq M$.
There is a property below based on derivation operator given $A_1, A_2 \subseteq G$.
$A_1\subseteq A_2 \implies A^{'}_2\subseteq A^{'}_1$
I will provide, by now, the proof for this property.
Proof: let's assume, for contradiction, $A^{'}_2\nsubseteq A^{'}_1$ is true. It implies that $m\in A^{'}_2$ and $m\notin A^{'}_1$. It leads to the statement of "m is a common attribute for the all objects in $A_2$, that is, $gIm \space \forall g \in A_2$". Since $A_1$ is a subset of $A_2$, $m$ is also common attribute for $\forall g \in A_1$. Thus $m\in A_1$ is true. This is a contradiction, since we have provided that $m$ is not in $A_1$ ($m\notin A^{'}_1$). $\qquad\square$