let x, y, z be Element of REAL+ ; :: thesis: ( x <=' y iff x + z <=' y + z )
thus ( x <=' y implies x + z <=' y + z ) :: thesis: ( x + z <=' y + z implies x <=' y )
proof
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;
(x + z) + z0 = y + z by A1, ARYTM_2:6;
hence x + z <=' y + z by ARYTM_2:19; :: thesis: verum
end;
assume x + z <=' y + z ; :: thesis: x <=' y
then consider z0 being Element of REAL+ such that
A2: (x + z) + z0 = y + z by ARYTM_2:9;
y + z = (x + z0) + z by A2, ARYTM_2:6;
hence x <=' y by ARYTM_2:11, ARYTM_2:19; :: thesis: verum