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 )