theorem :: TREES_1:14

for p, q, r being FinSequence st q ^ r in ProperPrefixes p holds
q in ProperPrefixes p