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