theorem Th32: :: SUBSTUT1:32

for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_universal holds
CQC_Sub S = Quant (S,(CQC_Sub (Sub_the_scope_of S)))