let T be Tree; :: thesis: ( T = {0,1} * implies for n being Nat holds 0* n in T -level n )

assume A1: T = {0,1} * ; :: thesis: for n being Nat holds 0* n in T -level n

let n be Nat; :: thesis: 0* n in T -level n

( len (0* n) = n & 0* n in T ) by A1, BINARI_3:4, CARD_1:def 7;

then 0* n in { w where w is Element of T : len w = n } ;

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

assume A1: T = {0,1} * ; :: thesis: for n being Nat holds 0* n in T -level n

let n be Nat; :: thesis: 0* n in T -level n

( len (0* n) = n & 0* n in T ) by A1, BINARI_3:4, CARD_1:def 7;

then 0* n in { w where w is Element of T : len w = n } ;

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