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