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

end;

assume A3: z in (-- A) \ (-- B) ; :: thesis: z in -- (A \ B)
then not z in -- B by XBOOLE_0:def 5;
then A4: not - z in B by Th12;
- z in A by A3, Th12;
then - z in A \ B by A4, XBOOLE_0:def 5;
hence z in -- (A \ B) by Th12; :: thesis: verum