let Z be Tree; :: thesis: for n, m being Element of NAT st n <= m & <*m*> in Z holds
<*n*> in Z
let n, m be Element of NAT ; :: thesis: ( n <= m & <*m*> in Z implies <*n*> in Z )
assume ( n <= m & <*m*> in Z ) ; :: thesis: <*n*> in Z
then A1: ( {} ^ <*m*> in Z & n <= m ) by FINSEQ_1:47;
reconsider s = {} as FinSequence of NAT by TREES_1:47;
s ^ <*n*> in Z by A1, TREES_1:def 5;
hence <*n*> in Z by FINSEQ_1:47; :: thesis: verum