dom (R | Y) = Y by RELAT_1:62;
hence not R | Y is empty ; :: thesis: verum