let A, B, C be complex-membered set ; :: thesis: A -- (B /\ C) c= (A -- B) /\ (A -- C)
A -- (B /\ C) = A ++ ((-- B) /\ (-- C)) by Th16;
hence A -- (B /\ C) c= (A -- B) /\ (A -- C) by Th49; :: thesis: verum