let X be ext-real-membered non empty set ; :: thesis: ( X is bounded_below & X <> {+infty} implies inf X in REAL )
assume A1: X is bounded_below ; :: thesis: ( not X <> {+infty} or inf X in REAL )
then consider r being Real such that
A2: r is LowerBound of X ;
assume X <> {+infty} ; :: thesis: inf X in REAL
then A3: ex x being Element of REAL st x in X by A1, Th50;
inf X is LowerBound of X by Def4;
then A4: inf X <> +infty by A3, Def2, XXREAL_0:9;
A5: r in REAL by XREAL_0:def 1;
r <= inf X by A2, Def4;
hence inf X in REAL by A5, A4, XXREAL_0:10; :: thesis: verum