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