theorem Th7: :: HUFFMAN1:7

for X being finite binary DecoratedTree of IndexedREAL holds LeavesSet {X} = {(Leaves X)}