for T being Tree
for p, q being FinSequence st p in T & q is_a_prefix_of p holds
q in T