theorem :: TREES_1:54

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