:: deftheorem defines |-| CQC_THE3:def 4 :
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 holds
( X |- p iff Y |- p ) );