theorem :: BINTREE2:6

for T being Tree st ( for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) holds
Leaves T = {}