let X be ext-real-membered non empty set ; :: thesis: ( ex y being UpperBound of X st y <> +infty implies X is bounded_above )
given y being UpperBound of X such that A1: y <> +infty ; :: thesis: X is bounded_above

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

suppose A2: y = -infty ; :: thesis: X is bounded_above

take 0 ; :: according to XXREAL_2:def 10 :: thesis: 0 is UpperBound of X
let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= 0 )
assume A3: x in X ; :: thesis: x <= 0
X c= {-infty} by A2, Th51;
hence x <= 0 by A3, TARSKI:def 1; :: thesis: verum

end;

suppose y <> -infty ; :: thesis: X is bounded_above

then y in REAL by A1, XXREAL_0:14;
then reconsider y = y as Real ;
take y ; :: according to XXREAL_2:def 10 :: thesis: y is UpperBound of X
thus y is UpperBound of X ; :: thesis: verum

end;

end;