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

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