let A, B, C be complex-membered set ; :: thesis: (A -- B) /// C c= (A /// C) -- (B /// C)
(A ++ (-- B)) /// C c= (A /// C) ++ ((-- B) /// C) by Th101;
hence (A -- B) /// C c= (A /// C) -- (B /// C) by Th100; :: thesis: verum