theorem Th15: :: DTCONSTR:15

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