theorem Th13: :: HUFFMAN1:13
for s, t being DecoratedTree
for x being object holds Leaves (x -tree (t,s)) = (Leaves t) \/ (Leaves s)