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 object holds
( x in A ^Fodelta iff x in (A ^Fob) \ (A ^Foi) )

proof

let x be object ; :: 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 Th39;
then x in (A ^Fob) /\ ((A ^Foi) `) by Th37;
hence x in (A ^Fob) \ (A ^Foi) by SUBSET_1:13; :: 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:13;
then x in (A ^Fob) /\ ((((A `) ^Fob) `) `) by Th37;
hence x in A ^Fodelta by Th39; :: thesis: verum

end;

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