rng (R * S) c= rng S by Th20;
hence not {} in rng (R * S) by Def7; :: according to RELAT_1:def 9 :: thesis: verum