:: deftheorem Def7 defines CQCQuant SUBLEMMA:def 7 :
for Al being QC-alphabet
for S1 being Element of CQC-Sub-WFF Al
for p being Element of CQC-WFF Al st S1 is Sub_universal & p = CQC_Sub (CQCSub_the_scope_of S1) holds
CQCQuant (S1,p) = Quant (S1,p);