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