theorem Th5: :: TREES_9:5

for t being Tree
for p being Element of t holds
( t | p = elementary_tree 0 iff p in Leaves t )