:: deftheorem Def10 defines NAT-to-PN DTCONSTR:def 10 :
for b₁ being sequence of (TS PeanoNat) holds
( b₁ = NAT-to-PN iff ( b₁ . 0 = root-tree 0 & ( for n being Nat holds b₁ . (n + 1) = PNsucc (b₁ . n) ) ) );