theorem Th9: :: TREES_9:9

for t being finite Tree
for p being Element of t st t = t | p holds
p = {}