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