rng R c= Y by RELAT_1:def 19;
hence Y | R = R null Y by RELAT_1:125; :: thesis: verum