R |_2 Y c= [:Y,Y:] by XBOOLE_1:17;
hence R |_2 Y is Relation of Y,Y by RELSET_1:def 1; :: thesis: verum