∀X,𝒢∀ℱ⊆𝒢(⟨ℱ⟩X⊆⟨𝒢⟩X)

$ \forall X,\mathcal G\forall\mathcal F\subseteq\mathcal G:\lang\mathcal F\rang_X\subseteq\lang\mathcal G\rang_X

$ \because\forall X,\mathcal F,\mathcal G:

$ \mathcal F\subseteq\mathcal G

$ \implies\forall F:

$ F\in\lang\mathcal F\rang_X

$ \iff F\in2^X\land\exist F'\subseteq F:F'\in\mathcal F

$ \implies F\in2^X\land\exist F'\subseteq F:F'\in\mathcal G

$ \because\mathcal F\subseteq\mathcal G

$ \iff F\in\lang\mathcal G\rang_X

$ \underline{\implies\lang\mathcal F\rang_X\subseteq\lang\mathcal G\rang_X\quad}_\blacksquare