let X be real-membered non empty set ; :: thesis: ( X is bounded_below implies inf X in REAL )
given r being real number such that G: r is LowerBound of X ; :: according to XXREAL_2:def 9 :: thesis: inf X in REAL
A: r <= inf X by Def4, G;
consider s being real number such that
W: s in X by MEMBERED:9;
F: ( r in REAL & s in REAL ) by XREAL_0:def 1;
inf X <= s by W, Th3;
hence inf X in REAL by A, F, XXREAL_0:45; :: thesis: verum