:: deftheorem DefU defines UpperBound COUNTERS:def 7 :
for X being ext-natural-membered set
for b₂ being object holds
( b₂ is UpperBound of X iff for N being ExtNat st N in X holds
N <= b₂ );