dom R c= Y by RELAT_1:def 18;
hence R | Y = R null Y by RELAT_1:68; :: thesis: verum