:: deftheorem defines CQC-WFF CQC_LANG:def 2 :
for A being QC-alphabet holds CQC-WFF A = { s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } ;