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