let FMT be non empty FMT_Space_Str ; :: thesis: for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob)

let A be Subset of FMT; :: thesis: A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob)

for x being Element of FMT holds

( x in A ^Fodelta iff x in (A ^Fob) /\ ((A `) ^Fob) )

let A be Subset of FMT; :: thesis: A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob)

for x being Element of FMT holds

( x in A ^Fodelta iff x in (A ^Fob) /\ ((A `) ^Fob) )

proof

hence
A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob)
by SUBSET_1:3; :: thesis: verum
let x be Element of FMT; :: thesis: ( x in A ^Fodelta iff x in (A ^Fob) /\ ((A `) ^Fob) )

thus ( x in A ^Fodelta implies x in (A ^Fob) /\ ((A `) ^Fob) ) :: thesis: ( x in (A ^Fob) /\ ((A `) ^Fob) implies x in A ^Fodelta )

then ( x in A ^Fob & x in (A `) ^Fob ) by XBOOLE_0:def 4;

then for W being Subset of FMT st W in U_FMT x holds

( W meets A & W meets A ` ) by Th20;

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

end;thus ( x in A ^Fodelta implies x in (A ^Fob) /\ ((A `) ^Fob) ) :: thesis: ( x in (A ^Fob) /\ ((A `) ^Fob) implies x in A ^Fodelta )

proof

assume
x in (A ^Fob) /\ ((A `) ^Fob)
; :: thesis: x in A ^Fodelta
assume A1:
x in A ^Fodelta
; :: thesis: x in (A ^Fob) /\ ((A `) ^Fob)

then for W being Subset of FMT st W in U_FMT x holds

W meets A ` by Th19;

then A2: x in (A `) ^Fob ;

for W being Subset of FMT st W in U_FMT x holds

W meets A by A1, Th19;

then x in A ^Fob ;

hence x in (A ^Fob) /\ ((A `) ^Fob) by A2, XBOOLE_0:def 4; :: thesis: verum

end;then for W being Subset of FMT st W in U_FMT x holds

W meets A ` by Th19;

then A2: x in (A `) ^Fob ;

for W being Subset of FMT st W in U_FMT x holds

W meets A by A1, Th19;

then x in A ^Fob ;

hence x in (A ^Fob) /\ ((A `) ^Fob) by A2, XBOOLE_0:def 4; :: thesis: verum

then ( x in A ^Fob & x in (A `) ^Fob ) by XBOOLE_0:def 4;

then for W being Subset of FMT st W in U_FMT x holds

( W meets A & W meets A ` ) by Th20;

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