:: deftheorem Def9 defines bounded_below XXREAL_2:def 9 :
for X being ext-real-membered set holds
( X is bounded_below iff ex r being Real st r is LowerBound of X );