theorem :: BINTREE1:3

for T being Tree
for t being Element of T holds
( succ t = {} iff t in Leaves T )