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 Th165
.= (-- (a -- A)) /\ (-- (a -- B)) by Th16
.= (-- (a -- A)) /\ (B -- a) by Th71
.= (A -- a) /\ (B -- a) by Th71 ; :: thesis: verum