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 ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) ) )

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

( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) ) )

let A be Subset of FMT; :: thesis: ( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) ) )

thus ( x in A ^Fon implies ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) ) ) :: thesis: ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) implies x in A ^Fon )

A1: x in A and

A2: for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ; :: thesis: x in A ^Fon

not x in A ^Fos by A2, Th22;

hence x in A ^Fon by A1, XBOOLE_0:def 5; :: thesis: verum

for A being Subset of FMT holds

( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) ) )

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

( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) ) )

let A be Subset of FMT; :: thesis: ( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) ) )

thus ( x in A ^Fon implies ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) ) ) :: thesis: ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) implies x in A ^Fon )

proof

assume that
assume
x in A ^Fon
; :: thesis: ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) )

then ( x in A & not x in A ^Fos ) by XBOOLE_0:def 5;

hence ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) ) ; :: thesis: verum

end;V \ {x} meets A ) )

then ( x in A & not x in A ^Fos ) by XBOOLE_0:def 5;

hence ( x in A & ( for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ) ) ; :: thesis: verum

A1: x in A and

A2: for V being Subset of FMT st V in U_FMT x holds

V \ {x} meets A ; :: thesis: x in A ^Fon

not x in A ^Fos by A2, Th22;

hence x in A ^Fon by A1, XBOOLE_0:def 5; :: thesis: verum