reconsider r = {} as Node of t by TREES_1:22;
( t . r = 0 or t . r = 1 ) by Lm2, TARSKI:def 2;
then A1: ( roots <*t*> = <*0*> or roots <*t*> = <*1*> ) by Th4;
nt = S by Lm15, TARSKI:def 1;
then nt -tree <*t*> in TS PeanoNat by A1, Def1, Lm5, Lm6;
hence nt -tree t is Element of TS PeanoNat by TREES_4:def 5; :: thesis: verum