( rng R c= {{}} & rng (R | X) c= rng R ) by Def13, Th53, XTUPLE_0:9;
hence rng (R | X) c= {{}} ; :: according to RELAT_1:def 15 :: thesis: verum