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