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