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

given y being UpperBound of X such that A1: y <> +infty ; :: thesis: X is bounded_above

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

end;

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;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

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;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