theorem Th18: :: CALCUL_2:18

for Al being QC-alphabet
for f, g being FinSequence of CQC-WFF Al holds f is_Subsequence_of g ^ f