let x be set ; :: thesis: for T being Tree st x in T holds
x is FinSequence of NAT
let T be Tree; :: thesis: ( x in T implies x is FinSequence of NAT )
assume A1: x in T ; :: thesis: x is FinSequence of NAT
T c= NAT * by Def5;
hence x is FinSequence of NAT by A1, FINSEQ_1:def 11; :: thesis: verum