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