:: deftheorem defines BoolBinFinTrees HUFFMAN1:def 3 :
for D being non empty set holds BoolBinFinTrees D = { x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } ;