let T be Tree; :: thesis: ( T = {0,1} * implies for n being non zero Nat

for y being Element of n -tuples_on BOOLEAN holds y in T -level n )

assume A1: T = {0,1} * ; :: thesis: for n being non zero Nat

for y being Element of n -tuples_on BOOLEAN holds y in T -level n

let n be non zero Nat; :: thesis: for y being Element of n -tuples_on BOOLEAN holds y in T -level n

let y be Element of n -tuples_on BOOLEAN; :: thesis: y in T -level n

y in { w where w is Element of T : len w = n } by A1;

hence y in T -level n by TREES_2:def 6; :: thesis: verum

for y being Element of n -tuples_on BOOLEAN holds y in T -level n )

assume A1: T = {0,1} * ; :: thesis: for n being non zero Nat

for y being Element of n -tuples_on BOOLEAN holds y in T -level n

let n be non zero Nat; :: thesis: for y being Element of n -tuples_on BOOLEAN holds y in T -level n

let y be Element of n -tuples_on BOOLEAN; :: thesis: y in T -level n

y in { w where w is Element of T : len w = n } by A1;

hence y in T -level n by TREES_2:def 6; :: thesis: verum