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