let A, B, C be complex-membered set ; :: thesis: A ** (B -- C) c= (A ** B) -- (A ** C)
A ** (B ++ (-- C)) c= (A ** B) ++ (A ** (-- C)) by Th95;
hence A ** (B -- C) c= (A ** B) -- (A ** C) by Th94; :: thesis: verum