theorem Th82: :: ARYTM_3:82

for r, s, t being Element of RAT+ st s <=' r holds
s *' t <=' r *' t