theorem :: SUBSTUT2:30

for Al being QC-alphabet
for n being Nat
for p, q being Element of CQC-WFF Al st QuantNbr p = n & q is_subformula_of p holds
QuantNbr q <= n