for W being Tree
for p, q being FinSequence of NAT
for C being Chain of W st p in C & q in C & len p <= len q holds
p is_a_prefix_of q