let A, B be complex-membered set ; :: thesis: -- (A /\ B) = (-- A) /\ (-- B)
let z be complex number ; :: according to MEMBERED:def 13 :: thesis: ( ( not z in -- (A /\ B) or z in (-- A) /\ (-- B) ) & ( not z in (-- A) /\ (-- B) or z in -- (A /\ B) ) )

hereby :: thesis: ( not z in (-- A) /\ (-- B) or z in -- (A /\ B) )

assume z in -- (A /\ B) ; :: thesis: z in (-- A) /\ (-- B)
then - z in A /\ B by Th18;
then ( - z in A & - z in B ) by XBOOLE_0:def 4;
then ( z in -- A & z in -- B ) by Th18;
hence z in (-- A) /\ (-- B) by XBOOLE_0:def 4; :: thesis: verum

end;

assume z in (-- A) /\ (-- B) ; :: thesis: z in -- (A /\ B)
then ( z in -- A & z in -- B ) by XBOOLE_0:def 4;
then ( - z in A & - z in B ) by Th18;
then - z in A /\ B by XBOOLE_0:def 4;
hence z in -- (A /\ B) by Th18; :: thesis: verum