let s, t be Element of RAT+ ; :: thesis: ( ( for r being Element of RAT+ holds
( r < s iff r < t ) ) implies s = t )
assume A1: for r being Element of RAT+ holds
( r < s iff r < t ) ; :: thesis: s = t
s <=' s ;
then A2: t <=' s by A1;
t <=' t ;
then s <=' t by A1;
hence s = t by A2, ARYTM_3:66; :: thesis: verum