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

proof

assume A4: y = -infty ; :: thesis: contradiction
then z + y = -infty by A2, Def2;
hence contradiction by A1, A3, A4, XXREAL_0:6; :: thesis: verum

end;

thus verum ; :: thesis: verum