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 & not x in (A \ {x}) ^Fob ) )
let x be Element of FMT; :: thesis: for A being Subset of FMT holds
( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) )
let A be Subset of FMT; :: thesis: ( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) )
A1: ( x in A & not x in (A \ {x}) ^Fob implies x in A ^Fos )

proof

assume that
A2: x in A and
A3: not x in (A \ {x}) ^Fob ; :: thesis: x in A ^Fos
consider V9 being Subset of FMT such that
A4: V9 in U_FMT x and
A5: V9 misses A \ {x} by A3;
V9 misses A /\ ({x} `) by A5, SUBSET_1:13;
then V9 /\ (A /\ ({x} `)) = {} ;
then (V9 /\ ({x} `)) /\ A = {} by XBOOLE_1:16;
then (V9 \ {x}) /\ A = {} by SUBSET_1:13;
then V9 \ {x} misses A ;
hence x in A ^Fos by A2, A4; :: thesis: verum

end;

( x in A ^Fos implies ( x in A & not x in (A \ {x}) ^Fob ) )

proof

assume A6: x in A ^Fos ; :: thesis: ( x in A & not x in (A \ {x}) ^Fob )
then consider V9 being Subset of FMT such that
A7: V9 in U_FMT x and
A8: V9 \ {x} misses A by Th22;
V9 /\ ({x} `) misses A by A8, SUBSET_1:13;
then (V9 /\ ({x} `)) /\ A = {} ;
then V9 /\ (({x} `) /\ A) = {} by XBOOLE_1:16;
then V9 misses ({x} `) /\ A ;
then V9 misses A \ {x} by SUBSET_1:13;
hence ( x in A & not x in (A \ {x}) ^Fob ) by A6, A7, Th20, Th22; :: thesis: verum

end;

hence ( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) ) by A1; :: thesis: verum