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

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

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;

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;

end;