thus ( X is bounded_below implies ex p being real number st
for r being real number st r in X holds
p <= r ) :: thesis: ( ex p being real number st
for r being real number st r in X holds
p <= r implies X is bounded_below )

proof

given p being real number such that G: p is LowerBound of X ; :: according to XXREAL_2:def 9 :: thesis: ex p being real number st
for r being real number st r in X holds
p <= r
reconsider p = p as Element of REAL by XREAL_0:def 1;
take p ; :: thesis: for r being real number st r in X holds
p <= r
let r be real number ; :: thesis: ( r in X implies p <= r )
thus ( r in X implies p <= r ) by G, XXREAL_2:def 2; :: thesis: verum

end;

given p being real number such that G: for r being real number st r in X holds
p <= r ; :: thesis: X is bounded_below
take p ; :: according to XXREAL_2:def 9 :: thesis: p is LowerBound of X
let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not r in X or p <= r )
assume r in X ; :: thesis: p <= r
hence p <= r by G; :: thesis: verum