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 )
reconsider CFX = clf FX, CGX = clf GX as set ;
assume A1: FX c= GX ; :: thesis: clf FX c= clf GX
for X being object st X in CFX holds
X in CGX
proof
let X be object ; :: 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 ;
ex V being Subset of T st
( X = Cl V & V in FX ) by A2, Def2;
hence X in CGX by A1, Def2; :: thesis: verum
end;
hence clf FX c= clf GX ; :: thesis: verum