theorem Th6: :: HUFFMAN1:6

for X being non empty finite Subset of (BinFinTrees IndexedREAL)
for s, t being finite binary DecoratedTree of IndexedREAL holds not MakeTree (t,s,((MaxVl X) + 1)) in X