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

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