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