:: deftheorem defines |- CQC_THE3:def 3 :
for A being QC-alphabet
for X being Subset of (CQC-WFF A) holds
( |- X iff for p being Element of CQC-WFF A st p in X holds
p is valid );