theorem Th20: :: TREES_1:21

for q being FinSequence of NAT
for T being Tree
for r being FinSequence st q ^ r in T holds
q in T