theorem :: CQC_THE3:16

for A being QC-alphabet holds |- TAUT A