theorem Th60: :: VALUED_1:61

for p being FinSequence
for q1, q2 being FinSubsequence st q1 c= p holds
ex ss being FinSubsequence st ss = q1 \/ (Shift (q2,(len p)))