( rng R c= {{} } & rng (R | X) c= rng R ) by Def15, Th99;
hence rng (R | X) c= {{} } by XBOOLE_1:1; :: according to RELAT_1:def 15 :: thesis: verum