:: deftheorem defines TAUT CQC_THE1:def 7 :
for Al being QC-alphabet holds TAUT Al = Cn ({} (CQC-WFF Al));