rng (R | X) c= rng R by RELAT_1:70;
hence R | X is non-zero ; :: thesis: verum