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:100;
then A2: (X |` R) | X c= (Y |` R) | X by RELAT_1:76;
(Y |` R) | X c= (Y |` R) | Y by A1, RELAT_1:75;
then (X |` R) | X c= (Y |` R) | Y by A2;
then R |_2 X c= (Y |` R) | Y by WELLORD1:10;
hence R |_2 X c= R |_2 Y by WELLORD1:10; :: thesis: verum