theorem Th7: :: BINTREE2:7

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