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 )

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

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

proof

hence
( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) )
by A1; :: thesis: verum
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;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