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 & not - z in B ) by XBOOLE_0:def 5;
then ( z in -- A & not z in -- B ) by Th18;
hence z in (-- A) \ (-- B) by XBOOLE_0:def 5; :: thesis: verum

end;

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