theorem :: PRE_CIRC:13

for q being DTree-yielding FinSequence
for k being Nat st k + 1 in dom q holds
<*k*> in tree (doms q)