:: deftheorem defines min COUNTERS:def 9 :
for X being left_end ext-natural-membered set
for b₂ being ExtNat holds
( b₂ = min X iff ( b₂ in X & ( for N being ExtNat st N in X holds
b₂ <= N ) ) );