let r, s, t be Element of RAT+ ; :: thesis: ( t <> {} & s *' t <=' r *' t implies s <=' r )
assume that
A1: t <> {} and
A2: s *' t <=' r *' t ; :: thesis: s <=' r
ex x being Element of RAT+ st
( s *' t = t *' x & x <=' r ) by A2, Th79;
hence s <=' r by A1, Th56; :: thesis: verum