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