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;
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;