:: deftheorem defines LeavesSet HUFFMAN1:def 11 :
for X being set holds LeavesSet X = { (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } ;