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

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