let T be binary Tree; :: thesis: for n being Element of NAT
for t being Element of T st t in T -level n holds
t is Tuple of n,BOOLEAN
let n be Element of NAT ; :: thesis: for t being Element of T st t in T -level n holds
t is Tuple of n,BOOLEAN
let t be Element of T; :: thesis: ( t in T -level n implies t is Tuple of n,BOOLEAN )
assume t in T -level n ; :: thesis: t is Tuple of n,BOOLEAN
then t in { w where w is Element of T : len w = n } by TREES_2:def 6;
then ex t2 being Element of T st
( t2 = t & len t2 = n ) ;
hence t is Tuple of n,BOOLEAN by FINSEQ_2:110; :: thesis: verum