the carrier of R \/ the carrier of S <> {} ;
hence not R [*] S is empty by Def2; :: thesis: verum