theorem :: MSSCYC_1:19

for t being DecoratedTree
for p being Node of t
for k being Element of NAT holds p | k is Node of t