theorem Th20: :: FIB_NUM2:20

for q being FinSubsequence ex p being FinSequence st q c= p