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 ^Fos implies ( x in A & not x in (A \ {x}) ^Fob ) )

proof

assume A2: x in A ^Fos ; :: thesis: ( x in A & not x in (A \ {x}) ^Fob )
then consider V' being Subset of FMT such that
A3: ( V' in U_FMT x & V' \ {x} misses A ) by Th23;
( V' in U_FMT x & V' /\ ({x} ` ) misses A ) by A3, SUBSET_1:32;
then (V' /\ ({x} ` )) /\ A = {} by XBOOLE_0:def 7;
then V' /\ (({x} ` ) /\ A) = {} by XBOOLE_1:16;
then ( V' in U_FMT x & V' misses ({x} ` ) /\ A ) by A3, XBOOLE_0:def 7;
then ( V' in U_FMT x & V' misses A \ {x} ) by SUBSET_1:32;
hence ( x in A & not x in (A \ {x}) ^Fob ) by A2, Th21, Th23; :: thesis: verum

end;

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

proof

assume that
A4: x in A and
A5: not x in (A \ {x}) ^Fob ; :: thesis: x in A ^Fos
consider V' being Subset of FMT such that
A6: ( V' in U_FMT x & V' misses A \ {x} ) by A5;
( V' in U_FMT x & V' misses A /\ ({x} ` ) ) by A6, SUBSET_1:32;
then ( V' in U_FMT x & V' /\ (A /\ ({x} ` )) = {} ) by XBOOLE_0:def 7;
then ( V' in U_FMT x & (V' /\ ({x} ` )) /\ A = {} ) by XBOOLE_1:16;
then ( V' in U_FMT x & (V' \ {x}) /\ A = {} ) by SUBSET_1:32;
then ( V' in U_FMT x & V' \ {x} misses A ) by XBOOLE_0:def 7;
hence x in A ^Fos by A4; :: thesis: verum

end;

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