let r, s, t be Element of RAT+ ; :: thesis: ( r <=' s & s <=' t implies r <=' t )
given x being Element of RAT+ such that A1: s = r + x ; :: according to ARYTM_3:def 13 :: thesis: ( not s <=' t or r <=' t )
given y being Element of RAT+ such that A2: t = s + y ; :: according to ARYTM_3:def 13 :: thesis: r <=' t
take x + y ; :: according to ARYTM_3:def 13 :: thesis: t = r + (x + y)
thus t = r + (x + y) by A1, A2, Th51; :: thesis: verum