let A, B be complex-membered set ; :: thesis: (A /\ B) "" = (A "" ) /\ (B "" )
let a be complex number ; :: 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 a " in A /\ B by Th35;
then ( a " in A & a " in B ) by XBOOLE_0:def 4;
then ( a in A "" & a in B "" ) by Th35;
hence a in (A "" ) /\ (B "" ) by XBOOLE_0:def 4; :: thesis: verum

end;

assume a in (A "" ) /\ (B "" ) ; :: thesis: a in (A /\ B) ""
then ( a in A "" & a in B "" ) by XBOOLE_0:def 4;
then ( a " in A & a " in B ) by Th35;
then a " in A /\ B by XBOOLE_0:def 4;
hence a in (A /\ B) "" by Th35; :: thesis: verum