theorem Th79: :: ARYTM_3:79

for r, s, t being Element of RAT+ st r <=' s *' t holds
ex t0 being Element of RAT+ st
( r = s *' t0 & t0 <=' t )