theorem :: SUBSTUT2:34

for Al being QC-alphabet
for p being Element of CQC-WFF Al st 1 <= QuantNbr p holds
ex q being Element of CQC-WFF Al st
( q is_subformula_of p & QuantNbr q = 1 ) by Th33;