:: deftheorem defines valid CQC_THE1:def 9 :
for Al being QC-alphabet
for s being QC-formula of Al holds
( s is valid iff {} (CQC-WFF Al) |- s );