let X be ext-real-membered non empty set ; :: thesis: ( ex y being LowerBound of X st y <> -infty implies X is bounded_below )

given y being LowerBound of X such that A1: y <> -infty ; :: thesis: X is bounded_below

given y being LowerBound of X such that A1: y <> -infty ; :: thesis: X is bounded_below

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

end;

suppose A2:
y = +infty
; :: thesis: X is bounded_below

take
0
; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of X

let x be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( x in X implies 0 <= x )

assume A3: x in X ; :: thesis: 0 <= x

X c= {+infty} by A2, Th52;

hence 0 <= x by A3, TARSKI:def 1; :: thesis: verum

end;let x be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( x in X implies 0 <= x )

assume A3: x in X ; :: thesis: 0 <= x

X c= {+infty} by A2, Th52;

hence 0 <= x by A3, TARSKI:def 1; :: thesis: verum

suppose
y <> +infty
; :: thesis: X is bounded_below

then
y in REAL
by A1, XXREAL_0:14;

then reconsider y = y as Real ;

take y ; :: according to XXREAL_2:def 9 :: thesis: y is LowerBound of X

thus y is LowerBound of X ; :: thesis: verum

end;then reconsider y = y as Real ;

take y ; :: according to XXREAL_2:def 9 :: thesis: y is LowerBound of X

thus y is LowerBound of X ; :: thesis: verum