let FMT be non empty FMT_Space_Str ; :: thesis: for A being Subset of FMT holds A ^Fodelta = (A ^Fob ) \ (A ^Foi )
let A be Subset of FMT; :: thesis: A ^Fodelta = (A ^Fob ) \ (A ^Foi )
for x being set holds
( x in A ^Fodelta iff x in (A ^Fob ) \ (A ^Foi ) )

proof

let x be set ; :: thesis: ( x in A ^Fodelta iff x in (A ^Fob ) \ (A ^Foi ) )
thus ( x in A ^Fodelta implies x in (A ^Fob ) \ (A ^Foi ) ) :: thesis: ( x in (A ^Fob ) \ (A ^Foi ) implies x in A ^Fodelta )

proof

assume x in A ^Fodelta ; :: thesis: x in (A ^Fob ) \ (A ^Foi )
then x in (A ^Fob ) /\ ((((A ` ) ^Fob ) ` ) ` ) by Th40;
then x in (A ^Fob ) /\ ((A ^Foi ) ` ) by Th38;
hence x in (A ^Fob ) \ (A ^Foi ) by SUBSET_1:32; :: thesis: verum

end;

assume x in (A ^Fob ) \ (A ^Foi ) ; :: thesis: x in A ^Fodelta
then x in (A ^Fob ) /\ ((A ^Foi ) ` ) by SUBSET_1:32;
then x in (A ^Fob ) /\ ((((A ` ) ^Fob ) ` ) ` ) by Th38;
hence x in A ^Fodelta by Th40; :: thesis: verum

end;

hence A ^Fodelta = (A ^Fob ) \ (A ^Foi ) by TARSKI:2; :: thesis: verum