rng R c= Y by Def19;
hence Y |` R = R by Th94; :: thesis: verum