:: deftheorem Def9 defines MaxVl HUFFMAN1:def 9 :
for X being non empty finite Subset of (BinFinTrees IndexedREAL)
for b₂ being Nat holds
( b₂ = MaxVl X iff ex L being non empty finite Subset of NAT st
( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b₂ = max L ) );