for Al being QC-alphabet
for p being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f & |- (Ant f) ^ <*('not' (Suc f))*> holds
|- (Ant f) ^ <*p*>