thus ( X is bounded_below implies ex UB being LowerBound of X st UB in REAL ) :: thesis: ( ex LB being LowerBound of X st LB in REAL implies X is bounded_below )

proof

given r being real number such that A1: r is LowerBound of X ; :: according to XXREAL_2:def 9 :: thesis: ex UB being LowerBound of X st UB in REAL
r in REAL by XREAL_0:def 1;
hence ex UB being LowerBound of X st UB in REAL by A1; :: thesis: verum

end;

given UB being LowerBound of X such that A2: UB in REAL ; :: thesis: X is bounded_below
reconsider UB = UB as real number by A2;
take UB ; :: according to XXREAL_2:def 9 :: thesis: UB is LowerBound of X
thus UB is LowerBound of X ; :: thesis: verum