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

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

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

hence inf A <> -infty by TW3; :: 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 Z: inf A <> -infty ; :: thesis: A is bounded_below

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

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

take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of A
A: +infty is LowerBound of A by S, Def4;
thus 0 is LowerBound of A by A, Th76; :: thesis: verum

end;

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

then reconsider r = inf A as real number ;
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;