let A, B be complex-membered set ; :: thesis: (A /\ B) "" = (A "") /\ (B "")
let a be Complex; :: according to MEMBERED:def 13 :: thesis: ( ( not a in (A /\ B) "" or a in (A "") /\ (B "") ) & ( not a in (A "") /\ (B "") or a in (A /\ B) "" ) )
hereby :: thesis: ( not a in (A "") /\ (B "") or a in (A /\ B) "" )
assume a in (A /\ B) "" ; :: thesis: a in (A "") /\ (B "")
then A1: a " in A /\ B by Th29;
then a " in B by XBOOLE_0:def 4;
then A2: a in B "" by Th29;
a " in A by A1, XBOOLE_0:def 4;
then a in A "" by Th29;
hence a in (A "") /\ (B "") by A2, XBOOLE_0:def 4; :: thesis: verum
end;
assume A3: a in (A "") /\ (B "") ; :: thesis: a in (A /\ B) ""
then a in B "" by XBOOLE_0:def 4;
then A4: a " in B by Th29;
a in A "" by A3, XBOOLE_0:def 4;
then a " in A by Th29;
then a " in A /\ B by A4, XBOOLE_0:def 4;
hence a in (A /\ B) "" by Th29; :: thesis: verum