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