let x, y, z be ExtReal; ( z in REAL & x < y implies ( x + z < y + z & x - z < y - z ) )
assume that
A1:
z in REAL
and
A2:
x < y
; ( x + z < y + z & x - z < y - z )
A3:
x + z <> y + z
proof
assume
x + z = y + z
;
contradiction
then x =
(y + z) - z
by A1, Th22
.=
y
by A1, Th22
;
hence
contradiction
by A2;
verum
end;
A4:
x - z <> y - z
proof
assume
x - z = y - z
;
contradiction
then x =
(y - z) + z
by A1, Th22
.=
y
by A1, Th22
;
hence
contradiction
by A2;
verum
end;
( x + z <= y + z & x - z <= y - z )
by A2, Th36;
hence
( x + z < y + z & x - z < y - z )
by A3, A4, XXREAL_0:1; verum