theorem :: TREES_1:55

for T being Tree
for t being Element of T holds
( t in Leaves T iff for n being Nat holds not t ^ <*n*> in T )