:: deftheorem Def23 defines max# MMLQUERY:def 23 :
for A being FinSequence
for b₂ being Nat holds
( b₂ = max# A iff ( ( for a being set holds #occurrences (a,A) <= b₂ ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
b₂ <= n ) ) );