let FMT be non empty FMT_Space_Str ; :: thesis: for A being Subset of FMT holds A ^Fodelta = (A ^Fodel_i) \/ (A ^Fodel_o)
let A be Subset of FMT; :: thesis: A ^Fodelta = (A ^Fodel_i) \/ (A ^Fodel_o)
for x being object holds
( x in A ^Fodelta iff x in (A ^Fodel_i) \/ (A ^Fodel_o) )

proof

let x be object ; :: thesis: ( x in A ^Fodelta iff x in (A ^Fodel_i) \/ (A ^Fodel_o) )
thus ( x in A ^Fodelta implies x in (A ^Fodel_i) \/ (A ^Fodel_o) ) :: thesis: ( x in (A ^Fodel_i) \/ (A ^Fodel_o) implies x in A ^Fodelta )

proof

assume x in A ^Fodelta ; :: thesis: x in (A ^Fodel_i) \/ (A ^Fodel_o)
then x in ([#] the carrier of FMT) /\ (A ^Fodelta) by XBOOLE_1:28;
then x in (A \/ (A `)) /\ (A ^Fodelta) by SUBSET_1:10;
hence x in (A ^Fodel_i) \/ (A ^Fodel_o) by XBOOLE_1:23; :: thesis: verum

end;

assume x in (A ^Fodel_i) \/ (A ^Fodel_o) ; :: thesis: x in A ^Fodelta
then x in (A \/ (A `)) /\ (A ^Fodelta) by XBOOLE_1:23;
then x in ([#] the carrier of FMT) /\ (A ^Fodelta) by SUBSET_1:10;
hence x in A ^Fodelta by XBOOLE_1:28; :: thesis: verum

end;

hence A ^Fodelta = (A ^Fodel_i) \/ (A ^Fodel_o) by TARSKI:2; :: thesis: verum