let x, y, z be ext-real number ; :: thesis: ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or ( y = +infty & z = -infty ) or ( y = -infty & z = +infty ) or not x - y <= z or y <> -infty )
assume that
A1: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) & not ( y = +infty & z = -infty ) & not ( y = -infty & z = +infty ) ) and
A2: x - y <= z ; :: thesis: y <> -infty
thus y <> -infty :: thesis: verum

proof

assume A3: y = -infty ; :: thesis: contradiction
then x - y = +infty by A1, Th14;
hence contradiction by A1, A2, A3, XXREAL_0:4; :: thesis: verum

end;

thus verum ; :: thesis: verum