let FX, GX be Subset-Family of PM; :: thesis: ( ( for V being Subset of PM holds
( V in FX iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ) & ( for V being Subset of PM holds
( V in GX iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ) implies FX = GX )
assume A1: for V being Subset of PM holds
( V in FX iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ; :: thesis: ( ex V being Subset of PM st
( ( V in GX implies for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) implies ( ( for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) & not V in GX ) ) or FX = GX )
assume A2: for W being Subset of PM holds
( W in GX iff for y being Element of PM st y in W holds
ex p being Real st
( p > 0 & Ball (y,p) c= W ) ) ; :: thesis: FX = GX
for Y being Subset of PM holds
( Y in FX iff Y in GX )

proof

let Y be Subset of PM; :: thesis: ( Y in FX iff Y in GX )

A3: now :: thesis: ( Y in GX implies Y in FX )

assume Y in GX ; :: thesis: Y in FX
then for x being Element of PM st x in Y holds
ex r being Real st
( r > 0 & Ball (x,r) c= Y ) by A2;
hence Y in FX by A1; :: thesis: verum

end;

now :: thesis: ( Y in FX implies Y in GX )

assume Y in FX ; :: thesis: Y in GX
then for x being Element of PM st x in Y holds
ex r being Real st
( r > 0 & Ball (x,r) c= Y ) by A1;
hence Y in GX by A2; :: thesis: verum

end;

hence ( Y in FX iff Y in GX ) by A3; :: thesis: verum

end;

hence FX = GX by SETFAM_1:31; :: thesis: verum