thus ( X is bounded_above implies ex UB being UpperBound of X st UB in REAL ) :: thesis: ( ex UB being UpperBound of X st UB in REAL implies X is bounded_above )

proof

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

end;

given UB being UpperBound of X such that Z: UB in REAL ; :: thesis: X is bounded_above
reconsider UB = UB as real number by Z;
take UB ; :: according to XXREAL_2:def 10 :: thesis: UB is UpperBound of X
thus UB is UpperBound of X ; :: thesis: verum