theorem Th8: :: BINTREE2:8

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