theorem Th12: :: BINTREE2:12

for T being full Tree
for n being non zero Nat holds Seg (2 to_power n) c= rng (NumberOnLevel (n,T))