:: deftheorem Def6 defines set_of_CQC-WFF-seq CALCUL_1:def 6 :
for Al being QC-alphabet
for b₂ being set holds
( b₂ = set_of_CQC-WFF-seq Al iff for a being object holds
( a in b₂ iff a is FinSequence of CQC-WFF Al ) );