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 Th101;
hence A ** (B -- C) c= (A ** B) -- (A ** C) by Th100; :: thesis: verum