let HX, GX be Subset-Family of ; :: thesis: ( ( for Z being Subset of holds
( Z in HX iff ex W being Subset of st
( Z = Cl W & W in FX ) ) ) & ( for Z being Subset of holds
( Z in GX iff ex W being Subset of st
( Z = Cl W & W in FX ) ) ) implies HX = GX )
assume that
A1: for Z being Subset of holds
( Z in HX iff ex W being Subset of st
( Z = Cl W & W in FX ) ) and
A2: for X being Subset of holds
( X in GX iff ex V being Subset of st
( X = Cl V & V in FX ) ) ; :: thesis: HX = GX

now

let X be set ; :: thesis: ( X in GX implies X in HX )
assume A3: X in GX ; :: thesis: X in HX
then reconsider X' = X as Subset of ;
ex V being Subset of st
( X' = Cl V & V in FX ) by A2, A3;
hence X in HX by A1; :: thesis: verum

end;

then A4: GX c= HX by TARSKI:def 3;

now

let Z be set ; :: thesis: ( Z in HX implies Z in GX )
assume A5: Z in HX ; :: thesis: Z in GX
then reconsider Z' = Z as Subset of ;
ex W being Subset of st
( Z' = Cl W & W in FX ) by A1, A5;
hence Z in GX by A2; :: thesis: verum

end;

then HX c= GX by TARSKI:def 3;
hence HX = GX by A4, XBOOLE_0:def 10; :: thesis: verum