let A, B be complex-membered set ; :: thesis: -- (A \+\ B) = (-- A) \+\ (-- B)
thus -- (A \+\ B) = (-- (A \ B)) \/ (-- (B \ A)) by Th21
.= ((-- A) \ (-- B)) \/ (-- (B \ A)) by Th23
.= (-- A) \+\ (-- B) by Th23 ; :: thesis: verum