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