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