:: deftheorem Def2 defines BinFinTrees HUFFMAN1:def 2 :
for D being non empty set
for b₂ being DTree-set of D holds
( b₂ = BinFinTrees D iff for T being DecoratedTree of D holds
( ( dom T is finite & T is binary ) iff T in b₂ ) );