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