for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al holds |- f ^ <*(VERUM Al)*>