:: deftheorem Def10 defines MinValueTree HUFFMAN1:def 10 :
for X being non empty finite Subset of (BinFinTrees IndexedREAL)
for b₂ being finite binary DecoratedTree of IndexedREAL holds
( b₂ is MinValueTree of X iff ( b₂ in X & ( for q being finite binary DecoratedTree of IndexedREAL st q in X holds
Vrootr b₂ <= Vrootr q ) ) );