theorem :: CQC_THE3:14

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