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

proof

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

A4: now

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

end;

now

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

end;

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

end;

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