let A, B be complex-membered set ; :: thesis: A /// (-- B) = -- (A /// B)
thus A /// (-- B) = A ** (-- (B "" )) by Th42
.= -- (A /// B) by Th100 ; :: thesis: verum