let A, B, C be complex-membered set ; :: thesis: A -- (B ++ C) = (A -- B) -- C
thus A -- (B ++ C) = A ++ ((-- B) -- C) by Lm5
.= (A -- B) -- C by Th50 ; :: thesis: verum