let x, y, z be Element of REAL+ ; :: thesis: ( x <=' y implies x *' z <=' y *' z )
assume x <=' y ; :: thesis: x *' z <=' y *' z
then consider z0 being Element of REAL+ such that
A1: x + z0 = y by ARYTM_2:9;
y *' z = (x *' z) + (z0 *' z) by A1, ARYTM_2:13;
hence x *' z <=' y *' z by ARYTM_2:19; :: thesis: verum