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

now :: thesis: for X being object st X in GX holds
X in HX

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

end;

then A4: GX c= HX ;

now :: thesis: for Z being object st Z in HX holds
Z in GX

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

end;

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