theorem Th10: :: BINTREE2:10

for T being Tree st T = {0,1} * holds
for n being Nat holds 0* n in T -level n