theorem Th21: :: TREES_2:21

for W being Tree
for v1, v2 being FinSequence
for C being Chain of W st v1 in C & v2 in C & not v1 in ProperPrefixes v2 holds
v2 is_a_prefix_of v1