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 A1: A is bounded_below ; :: thesis: inf A <> -infty

per cases ( A = {} or A = {+infty} or inf A in REAL ) by A1, Th58;

suppose A = {} ; :: thesis: inf A <> -infty

hence inf A <> -infty by Th38; :: thesis: verum

end;

suppose A = {+infty} ; :: thesis: inf A <> -infty

hence inf A <> -infty by Lm2; :: thesis: verum

end;

suppose inf A in REAL ; :: thesis: inf A <> -infty

hence inf A <> -infty ; :: thesis: verum

end;

end;

end;

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

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

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;

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;

end;