theorem Th17: :: DTCONSTR:17

for t being Element of TS PeanoNat holds PostTraversal t = <*0*> ^ ((height (dom t)) |-> 1)