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) )

proof

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 )

proof

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;

assume x in (A ^Fob) /\ ((A `) ^Fob) ; :: thesis: 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;

hence A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob) by SUBSET_1:3; :: thesis: verum