for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st Ant f |= p '&' q holds
Ant f |= p