let T be Tree; :: thesis: ( T = {0 ,1} * implies for n being non empty Element of NAT
for y being Tuple of n,BOOLEAN holds y in T -level n )
assume A1: T = {0 ,1} * ; :: thesis: for n being non empty Element of NAT
for y being Tuple of n,BOOLEAN holds y in T -level n
let n be non empty Element of NAT ; :: thesis: for y being Tuple of n,BOOLEAN holds y in T -level n
let y be Tuple of n,BOOLEAN ; :: thesis: y in T -level n
A2: len y = n by FINSEQ_1:def 18;
y in T by A1, FINSEQ_1:def 11;
then y in { w where w is Element of T : len w = n } by A2;
hence y in T -level n by TREES_2:def 6; :: thesis: verum