let A, B be complex-membered set ; :: thesis: -- (A \/ B) = (-- A) \/ (-- B)
let z be Complex; :: 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 Th12;
then ( - z in A or - z in B ) by XBOOLE_0:def 3;
then ( z in -- A or z in -- B ) by Th12;
hence z in (-- A) \/ (-- B) by XBOOLE_0:def 3; :: thesis: verum

end;

assume z in (-- A) \/ (-- B) ; :: thesis: z in -- (A \/ B)
then ( z in -- A or z in -- B ) by XBOOLE_0:def 3;
then ( - z in A or - z in B ) by Th12;
then - z in A \/ B by XBOOLE_0:def 3;
hence z in -- (A \/ B) by Th12; :: thesis: verum