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 number such that
A2: r is LowerBound of X by Def9;
X: r in REAL by XREAL_0:def 1;
A3: r <= inf X by A2, Def4;
assume X <> {+infty } ; :: thesis: inf X in REAL
then consider x being Element of REAL such that
A4: x in X by A1, Th50;
inf X is LowerBound of X by Def4;
then inf X <> +infty by A4, Def2, XXREAL_0:9;
hence inf X in REAL by A3, X, XXREAL_0:10; :: thesis: verum