let r, s, t be Element of RAT+ ; :: thesis: ( r <=' s & s <=' r + t implies ex t0 being Element of RAT+ st
( s = r + t0 & t0 <=' t ) )
given t0 being Element of RAT+ such that A1: s = r + t0 ; :: according to ARYTM_3:def 13 :: thesis: ( not s <=' r + t or ex t0 being Element of RAT+ st
( s = r + t0 & t0 <=' t ) )
assume s <=' r + t ; :: thesis: ex t0 being Element of RAT+ st
( s = r + t0 & t0 <=' t )
then t0 <=' t by A1, Th83;
hence ex t0 being Element of RAT+ st
( s = r + t0 & t0 <=' t ) by A1; :: thesis: verum