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

proof

given p being real number such that G: p is UpperBound of X ; :: according to XXREAL_2:def 10 :: thesis: ex p being real number st
for r being real number st r in X holds
r <= p
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
r <= p
let r be real number ; :: thesis: ( r in X implies r <= p )
thus ( r in X implies r <= p ) by G, XXREAL_2:def 1; :: thesis: verum

end;

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