:: deftheorem Def10 defines bounded_above XXREAL_2:def 10 :
for X being ext-real-membered set holds
( X is bounded_above iff ex r being Real st r is UpperBound of X );