:: deftheorem defines PNsucc DTCONSTR:def 9 :
for x being Element of TS PeanoNat holds PNsucc x = 1 -tree <*x*>;