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