for A being QC-alphabet holds {} (CQC-WFF A) |- TAUT A by Th13;