for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al st len f > 1 holds
len (Ant f) > 0