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