let s, t, r be Element of RAT+ ; :: thesis: ( s + t <=' r + t iff s <=' r )
thus ( s + t <=' r + t implies s <=' r ) :: thesis: ( s <=' r implies s + t <=' r + t )

proof

given z being Element of RAT+ such that A1: r + t = (s + t) + z ; :: according to ARYTM_3:def 13 :: thesis: s <=' r
take z ; :: according to ARYTM_3:def 13 :: thesis: r = s + z
r + t = (s + z) + t by A1, Th57;
hence r = s + z by Th69; :: thesis: verum

end;

given z being Element of RAT+ such that A2: r = s + z ; :: according to ARYTM_3:def 13 :: thesis: s + t <=' r + t
take z ; :: according to ARYTM_3:def 13 :: thesis: r + t = (s + t) + z
thus r + t = (s + t) + z by A2, Th57; :: thesis: verum