let Al be QC-alphabet ; :: thesis: for n being Nat
for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds
QuantNbr q = n ) holds
n = 0

let n be Nat; :: 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
QuantNbr q = n ) holds
n = 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
QuantNbr q = n ) implies n = 0 )

assume A1: for q being Element of CQC-WFF Al st q is_subformula_of p holds
QuantNbr q = n ; :: thesis: n = 0
defpred S1[ Element of CQC-WFF Al] means ( \$1 is_subformula_of p implies QuantNbr \$1 = 0 );
A2: for x being bound_QC-variable of Al
for r being Element of CQC-WFF Al st S1[r] holds
S1[ All (x,r)]
proof
let x be bound_QC-variable of Al; :: thesis: for r being Element of CQC-WFF Al st S1[r] holds
S1[ All (x,r)]

let r be Element of CQC-WFF Al; :: thesis: ( S1[r] implies S1[ All (x,r)] )
assume S1[r] ; :: thesis: S1[ All (x,r)]
now :: thesis: not All (x,r) is_subformula_of pend;
hence S1[ All (x,r)] ; :: thesis: verum
end;
A5: 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 A11: 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 ;
A12: for r being Element of CQC-WFF Al holds S1[r] from QuantNbr p = n by A1;
hence n = 0 by A12; :: thesis: verum