let x, y, z be Element of REAL+ ; :: thesis: ( x *' y <=' x *' z & x <> {} implies y <=' z )
reconsider u = one as Element of REAL+ by ARYTM_2:20;
assume x *' y <=' x *' z ; :: thesis: ( not x <> {} or y <=' z )
then consider z0 being Element of REAL+ such that
A1: (x *' y) + z0 = x *' z by ARYTM_2:9;
assume A2: x <> {} ; :: thesis: y <=' z
then consider x1 being Element of REAL+ such that
A3: x *' x1 = one by ARYTM_2:14;
x *' z = (x *' y) + (u *' z0) by A1, ARYTM_2:15
.= (x *' y) + (x *' (x1 *' z0)) by A3, ARYTM_2:12
.= x *' (y + (x1 *' z0)) by ARYTM_2:13 ;
hence y <=' z by A2, Lm1, ARYTM_2:19; :: thesis: verum