let i, j be ordinal Element of RAT+ ; :: thesis: ( i in j implies i < j )
A1: j in omega by ARYTM_3:31;
i in omega by ARYTM_3:31;
then reconsider x = i, y = j as Element of REAL+ by A1, ARYTM_2:2;
assume A2: i in j ; :: thesis: i < j
then x <=' y by A1, ARYTM_2:18;
then A3: ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x9 <=' y9 ) by ARYTM_2:def 5;
i <> j by A2;
hence i < j by A3, ARYTM_3:66; :: thesis: verum