let A, B, C be complex-membered set ; :: thesis: A -- (B \/ C) = (A -- B) \/ (A -- C)
thus A -- (B \/ C) = A ++ ((-- B) \/ (-- C)) by Th15
.= (A -- B) \/ (A -- C) by Th48 ; :: thesis: verum