for Al being QC-alphabet
for i, n being Nat
for p, q being Element of CQC-WFF Al
for L being PATH of q,p st QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L holds
ex r being Element of CQC-WFF Al st
( r = L . i & QuantNbr r <= n )