let A, B be complex-membered set ; :: thesis: for a being Complex holds a -- (A \ B) = (a -- A) \ (a -- B)
let a be Complex; :: thesis: a -- (A \ B) = (a -- A) \ (a -- B)
thus a -- (A \ B) = a ++ ((-- A) \ (-- B)) by Th17
.= (a ++ (-- A)) \ (a ++ (-- B)) by Th150
.= (a -- A) \ (a -- B) ; :: thesis: verum