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 set ; :: 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 Th26, XBOOLE_1:7;
hence x in (A \/ B) ^Foi by A1; :: thesis: verum