let t, s, r be Element of RAT+ ; :: thesis: ( t <> {} & s *' t <=' r *' t implies s <=' r )
assume A1: ( t <> {} & s *' t <=' r *' t ) ; :: thesis: s <=' r
then consider x being Element of RAT+ such that
A2: ( s *' t = t *' x & x <=' r ) by Th87;
thus s <=' r by A1, A2, Th62; :: thesis: verum