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 Th95;
hence (A -- B) /// C c= (A /// C) -- (B /// C) by Th94; :: thesis: verum