let i, j be ordinal Element of RAT+ ; :: thesis: ( i c= j implies i <=' j )
assume i c= j ; :: thesis: i <=' j
then consider C being Ordinal such that
A1: j = i +^ C by ORDINAL3:27;
C in omega by A1, ORDINAL3:74;
then reconsider C = C as Element of RAT+ by Lm1;
j = i + C by A1, ARYTM_3:58;
hence i <=' j ; :: thesis: verum