let X be real-membered non empty set ; :: thesis: ( X is bounded_below implies inf X in REAL )

given r being Real such that A1: r is LowerBound of X ; :: according to XXREAL_2:def 9 :: thesis: inf X in REAL

consider s being Real such that

A2: s in X by MEMBERED:9;

A3: inf X <= s by A2, Th3;

A4: r in REAL by XREAL_0:def 1;

A5: s in REAL by XREAL_0:def 1;

r <= inf X by A1, Def4;

hence inf X in REAL by A4, A5, A3, XXREAL_0:45; :: thesis: verum

given r being Real such that A1: r is LowerBound of X ; :: according to XXREAL_2:def 9 :: thesis: inf X in REAL

consider s being Real such that

A2: s in X by MEMBERED:9;

A3: inf X <= s by A2, Th3;

A4: r in REAL by XREAL_0:def 1;

A5: s in REAL by XREAL_0:def 1;

r <= inf X by A1, Def4;

hence inf X in REAL by A4, A5, A3, XXREAL_0:45; :: thesis: verum