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