:: deftheorem defines CFQ SUBSTUT2:def 2 :
for Al being QC-alphabet holds CFQ Al = (QSub Al) | (CQC-Sub-WFF Al);