:: deftheorem defines CQC-Sub-WFF SUBSTUT1:def 39 :
for A being QC-alphabet holds CQC-Sub-WFF A = { S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } ;