:: deftheorem defines real-bounded XXREAL_2:def 11 :
for X being ext-real-membered set holds
( X is real-bounded iff ( X is bounded_below & X is bounded_above ) );