for W being Tree
for p, q being FinSequence of NAT
for B being Branch of W st p is_a_prefix_of q & q in B holds
p in B