let x, y be ext-real number ; :: thesis: ( 0 < x & x < y implies 0 < y - x )
assume A1: ( 0 < x & x < y ) ; :: thesis: 0 < y - x
then A2: x in REAL by XXREAL_0:48;
B3: 0 + x < y by A1, Tx3;
0 <> y - x

proof

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

end;

hence 0 < y - x by B3, A2, MEA2; :: thesis: verum