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