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