let s, r, 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 y = x *' t; :: according to ARYTM_3:def 13 :: thesis: r *' t = (s *' t) + y
thus r *' t = (s *' t) + y by A1, Th63; :: thesis: verum