:: deftheorem defines valid CQC_THE1:def 10 :
for Al being QC-alphabet
for s being QC-formula of Al holds
( s is valid iff s in TAUT Al );