let x, y be R_eal; :: 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, SUPINF_2:6; :: thesis: verum

end;

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

now

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

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

hence 0. < y - x by A2, SUPINF_2:7; :: thesis: verum

end;

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

y <= +infty by XXREAL_0:4;
then reconsider a = x as Real by A1, A4, XXREAL_0:14;
reconsider b = y as Real by A2, A3, XXREAL_0:14;
b - a > 0 by A1, XREAL_1:52;
hence 0. < y - x by SUPINF_2:5; :: thesis: verum

end;

end;

end;

hence 0. < y - x ; :: thesis: verum

end;

end;