let FMT be non empty FMT_Space_Str ; :: thesis: for A, B being Subset of FMT holds (A ^Foi) \/ (B ^Foi) c= (A \/ B) ^Foi
let A, B be Subset of FMT; :: thesis: (A ^Foi) \/ (B ^Foi) c= (A \/ B) ^Foi
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A ^Foi) \/ (B ^Foi) or x in (A \/ B) ^Foi )
assume x in (A ^Foi) \/ (B ^Foi) ; :: thesis: x in (A \/ B) ^Foi
then A1: ( x in A ^Foi or x in B ^Foi ) by XBOOLE_0:def 3;
( A ^Foi c= (A \/ B) ^Foi & B ^Foi c= (B \/ A) ^Foi ) by Th25, XBOOLE_1:7;
hence x in (A \/ B) ^Foi by A1; :: thesis: verum