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 A1: 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 A2: 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 )
A3: now :: thesis: ( Y in GX implies Y in FX )
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 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 Point of V 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