:: deftheorem Def2 defines LowerBound XXREAL_2:def 2 :
for X being ext-real-membered set
for b₂ being ExtReal holds
( b₂ is LowerBound of X iff for x being ExtReal st x in X holds
b₂ <= x );