let A be ext-real-membered set ; :: thesis: ( A is bounded_below iff inf A <> -infty )

hereby :: thesis: ( inf A <> -infty implies A is bounded_below )

assume A2:
inf A <> -infty
; :: thesis: A is bounded_below assume A1:
A is bounded_below
; :: thesis: inf A <> -infty

end;per cases
( inf A = +infty or inf A in REAL )
by A2, XXREAL_0:14;

end;

suppose A3:
inf A = +infty
; :: thesis: A is bounded_below

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

+infty is LowerBound of A by A3, Def4;

hence 0 is LowerBound of A by Th72; :: thesis: verum

end;+infty is LowerBound of A by A3, Def4;

hence 0 is LowerBound of A by Th72; :: thesis: verum

suppose
inf A in REAL
; :: thesis: A is bounded_below

then reconsider r = inf A as Real ;

take r ; :: according to XXREAL_2:def 9 :: thesis: r is LowerBound of A

thus r is LowerBound of A by Def4; :: thesis: verum

end;take r ; :: according to XXREAL_2:def 9 :: thesis: r is LowerBound of A

thus r is LowerBound of A by Def4; :: thesis: verum