let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds
for x being bound_QC-variable of Al
for r being Element of CQC-WFF Al holds q <> All (x,r) ) holds
QuantNbr p = 0

let p be Element of CQC-WFF Al; :: thesis: ( ( for q being Element of CQC-WFF Al st q is_subformula_of p holds
for x being bound_QC-variable of Al
for r being Element of CQC-WFF Al holds q <> All (x,r) ) implies QuantNbr p = 0 )

assume A1: for q being Element of CQC-WFF Al st q is_subformula_of p holds
for x being bound_QC-variable of Al
for r being Element of CQC-WFF Al holds q <> All (x,r) ; :: thesis:
defpred S1[ Element of CQC-WFF Al] means ( \$1 is_subformula_of p implies QuantNbr \$1 = 0 );
A2: for r, s being Element of CQC-WFF Al st S1[r] & S1[s] holds
S1[r '&' s]
proof end;
for r being Element of CQC-WFF Al st S1[r] holds
S1[ 'not' r]
proof end;
then A8: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S1[ VERUM Al] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) ) by ;
for r being Element of CQC-WFF Al holds S1[r] from hence QuantNbr p = 0 ; :: thesis: verum