let T be non empty TopSpace; :: thesis: for FX, GX being Subset-Family of T st FX c= GX holds
clf FX c= clf GX
let FX, GX be Subset-Family of T; :: thesis: ( FX c= GX implies clf FX c= clf GX )
assume A1: FX c= GX ; :: thesis: clf FX c= clf GX
reconsider CFX = clf FX, CGX = clf GX as set ;
for X being set st X in CFX holds
X in CGX

proof

let X be set ; :: thesis: ( X in CFX implies X in CGX )
assume A2: X in CFX ; :: thesis: X in CGX
then reconsider X = X as Subset of T ;
consider V being Subset of T such that
A3: X = Cl V and
A4: V in FX by A2, Def3;
thus X in CGX by A1, A3, A4, Def3; :: thesis: verum

end;

hence clf FX c= clf GX by TARSKI:def 3; :: thesis: verum