for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al st S is Sub_universal holds
CQC_Sub S = CQCQuant (S,(CQC_Sub (CQCSub_the_scope_of S)))