theorem :: ARYTM_3:95

for r, t being Element of RAT+ st t <> {} holds
ex s being Element of RAT+ st
( s in omega & r <=' s *' t )