let r, s, t 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, Th51;
hence r = s + z by Th62; :: 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, Th51; :: thesis: verum