let x, y be ext-real number ; :: thesis: ( x < y & x < +infty & -infty < y implies 0 < y - x )
assume that
A1: x < y and
A2: ( x < +infty & -infty < y ) ; :: thesis: 0 < y - x

per cases ( y = +infty or y <> +infty ) ;

suppose y = +infty ; :: thesis: 0 < y - x

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

end;

suppose A3: y <> +infty ; :: thesis: 0 < y - x

per cases ( x = -infty or x <> -infty ) ;

suppose x = -infty ; :: thesis: 0 < y - x

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

end;

suppose A4: x <> -infty ; :: thesis: 0 < y - x

( x in REAL & y in REAL ) by A2, A3, A4, XXREAL_0:14;
then reconsider a = x, b = y as real number ;
b - a > 0 by A1, XREAL_1:52;
hence 0 < y - x ; :: thesis: verum

end;

end;

end;

end;