let x, y be ExtReal; :: thesis: ( 0 < x & x < y implies 0 < y - x )
assume that
A1: 0 < x and
A2: x < y ; :: thesis: 0 < y - x
A3: x in REAL by A1, A2, XXREAL_0:48;
A4: 0 <> y - x

proof

assume 0 = y - x ; :: thesis: contradiction
then x = (y - x) + x by Th4
.= y by A3, Th22 ;
hence contradiction by A2; :: thesis: verum

end;

0 + x < y by A2, Th4;
hence 0 < y - x by A3, A4, Th45; :: thesis: verum