let FMT be non empty FMT_Space_Str ; :: thesis: for x being Element of FMT

for A being Subset of FMT holds

( x in A ^Fos iff ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) )

let x be Element of FMT; :: thesis: for A being Subset of FMT holds

( x in A ^Fos iff ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) )

let A be Subset of FMT; :: thesis: ( x in A ^Fos iff ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) )

thus ( x in A ^Fos implies ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) ) :: thesis: ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) implies x in A ^Fos )

( V in U_FMT x & V \ {x} misses A ) ) ; :: thesis: x in A ^Fos

hence x in A ^Fos ; :: thesis: verum

for A being Subset of FMT holds

( x in A ^Fos iff ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) )

let x be Element of FMT; :: thesis: for A being Subset of FMT holds

( x in A ^Fos iff ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) )

let A be Subset of FMT; :: thesis: ( x in A ^Fos iff ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) )

thus ( x in A ^Fos implies ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) ) :: thesis: ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) implies x in A ^Fos )

proof

assume
( x in A & ex V being Subset of FMT st
assume
x in A ^Fos
; :: thesis: ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) )

then ex y being Element of FMT st

( y = x & y in A & ex V being Subset of FMT st

( V in U_FMT y & V \ {y} misses A ) ) ;

hence ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) ; :: thesis: verum

end;( V in U_FMT x & V \ {x} misses A ) )

then ex y being Element of FMT st

( y = x & y in A & ex V being Subset of FMT st

( V in U_FMT y & V \ {y} misses A ) ) ;

hence ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) ; :: thesis: verum

( V in U_FMT x & V \ {x} misses A ) ) ; :: thesis: x in A ^Fos

hence x in A ^Fos ; :: thesis: verum