rng R c= Y by Def17;
hence Y |` R = R by Th88; :: thesis: verum