R .: Y = rng (R | Y) by RELAT_1:115;
hence not R .: Y is empty ; :: thesis: verum