let R be Relation; :: thesis: for X, Y being set st X c= Y holds
R |_2 X c= R |_2 Y
let X, Y be set ; :: thesis: ( X c= Y implies R |_2 X c= R |_2 Y )
assume A1: X c= Y ; :: thesis: R |_2 X c= R |_2 Y
then X | R c= Y | R by RELAT_1:131;
then A2: (X | R) | X c= (Y | R) | X by RELAT_1:105;
(Y | R) | X c= (Y | R) | Y by A1, RELAT_1:104;
then (X | R) | X c= (Y | R) | Y by A2, XBOOLE_1:1;
then R |_2 X c= (Y | R) | Y by WELLORD1:17;
hence R |_2 X c= R |_2 Y by WELLORD1:17; :: thesis: verum