theorem Th3: :: BINTREE2:3

for T being Tree st T = {0,1} * holds
T is binary