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