( rng R c= NAT & rng (R | X) c= rng R ) by Def4, RELAT_1:70;
hence rng (R | X) c= NAT ; :: according to VALUED_0:def 6 :: thesis: verum