let x, y be R_eal; :: thesis: ( 0. < x & x < y implies 0. < y - x )
assume A1: ( 0. < x & x < y ) ; :: thesis: 0. < y - x
then A2: x is Real by XXREAL_0:48;
0. + x < y by A1, SUPINF_2:18;
then A3: 0. <= y - x by A2, MEASURE4:2;
0. <> y - x

proof

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

end;

hence 0. < y - x by A3, XXREAL_0:1; :: thesis: verum