let z, x, y be ext-real number ; :: thesis: ( z in REAL & x < y implies ( x + z < y + z & x - z < y - z ) )
assume A1: ( z in REAL & x < y ) ; :: thesis: ( x + z < y + z & x - z < y - z )
then A2: ( x + z <= y + z & x - z <= y - z ) by Th36;
A3: x + z <> y + z

proof

assume x + z = y + z ; :: thesis: contradiction
then x = (y + z) - z by A1, Th44
.= y by A1, Th44 ;
hence contradiction by A1; :: thesis: verum

end;

x - z <> y - z

proof

assume x - z = y - z ; :: thesis: contradiction
then x = (y - z) + z by A1, Th44
.= y by A1, Th44 ;
hence contradiction by A1; :: thesis: verum

end;

hence ( x + z < y + z & x - z < y - z ) by A2, A3, XXREAL_0:1; :: thesis: verum