let x, y be ExtReal; :: thesis: ( x < y & x < +infty & -infty < y implies 0 < y - x )
assume that
A1: x < y and
A2: x < +infty and
A3: -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, Th13; :: thesis: verum

end;

suppose A4: 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 A3, Th14; :: thesis: verum

end;

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

A6: y in REAL by A3, A4, XXREAL_0:14;
x in REAL by A2, A5, XXREAL_0:14;
then reconsider a = x, b = y as Real by A6;
b - a > 0 by A1, XREAL_1:50;
hence 0 < y - x ; :: thesis: verum

end;

end;

end;

end;