theorem Th9: :: HUFFMAN1:9

for s, t being Tree holds not {} in Leaves (tree (t,s))