let i, j be ordinal Element of RAT+ ; :: thesis: ( i in j implies i < j )
A1: ( i in omega & j in omega ) by ARYTM_3:37;
then reconsider x = i, y = j as Element of REAL+ by ARYTM_2:2;
assume A2: i in j ; :: thesis: i < j
then x <=' y by A1, ARYTM_2:19;
then consider x', y' being Element of RAT+ such that
A3: ( x = x' & y = y' ) and
A4: x' <=' y' by ARYTM_2:def 5;
i <> j by A2;
hence i < j by A3, A4, ARYTM_3:73; :: thesis: verum