theorem Th11: :: BINTREE2:11

for T being Tree st T = {0,1} * holds
for n being non zero Nat
for y being Element of n -tuples_on BOOLEAN holds y in T -level n