:: deftheorem defines is_Subsequence_of CALCUL_1:def 4 :
for Al being QC-alphabet
for f, g being FinSequence of CQC-WFF Al holds
( f is_Subsequence_of g iff ex N being Subset of NAT st f c= Seq (g | N) );