theorem :: CQC_SIM1:18

for A being QC-alphabet
for p being Element of CQC-WFF A
for x being Element of bound_QC-variables A holds QuantNbr (All (x,p)) = (QuantNbr p) + 1