let n be Element of NAT ; :: thesis: for p being Element of CQC-WFF st ( for q being Element of CQC-WFF st q is_subformula_of p holds
QuantNbr q = n ) holds
n = 0
let p be Element of CQC-WFF ; :: thesis: ( ( for q being Element of CQC-WFF st q is_subformula_of p holds
QuantNbr q = n ) implies n = 0 )
assume A1: for q being Element of CQC-WFF st q is_subformula_of p holds
QuantNbr q = n ; :: thesis: n = 0
defpred S₁[ Element of CQC-WFF ] means ( $1 is_subformula_of p implies QuantNbr $1 = 0 );
A2: for r being Element of CQC-WFF st S₁[r] holds
S₁[ 'not' r]

proof

let r be Element of CQC-WFF ; :: thesis: ( S₁[r] implies S₁[ 'not' r] )
assume A3: S₁[r] ; :: thesis: S₁[ 'not' r]
assume A4: 'not' r is_subformula_of p ; :: thesis: QuantNbr ('not' r) = 0
r is_immediate_constituent_of 'not' r by QC_LANG2:60;
then r is_proper_subformula_of p by A4, QC_LANG2:83;
hence QuantNbr ('not' r) = 0 by A3, CQC_SIM1:16, QC_LANG2:def 22; :: thesis: verum

end;

A5: for r, s being Element of CQC-WFF st S₁[r] & S₁[s] holds
S₁[r '&' s]

proof

let r, s be Element of CQC-WFF ; :: thesis: ( S₁[r] & S₁[s] implies S₁[r '&' s] )
assume A6: ( S₁[r] & S₁[s] ) ; :: thesis: S₁[r '&' s]
assume A7: r '&' s is_subformula_of p ; :: thesis: QuantNbr (r '&' s) = 0
( r is_immediate_constituent_of r '&' s & s is_immediate_constituent_of r '&' s ) by QC_LANG2:62;
then ( r is_proper_subformula_of p & s is_proper_subformula_of p ) by A7, QC_LANG2:83;
then QuantNbr (r '&' s) = 0 + 0 by A6, CQC_SIM1:17, QC_LANG2:def 22;
hence QuantNbr (r '&' s) = 0 ; :: thesis: verum

end;

for x being bound_QC-variable
for r being Element of CQC-WFF st S₁[r] holds
S₁[ All x,r]

proof

let x be bound_QC-variable; :: thesis: for r being Element of CQC-WFF st S₁[r] holds
S₁[ All x,r]
let r be Element of CQC-WFF ; :: thesis: ( S₁[r] implies S₁[ All x,r] )
assume S₁[r] ; :: thesis: S₁[ All x,r]

now

assume A8: All x,r is_subformula_of p ; :: thesis: contradiction
r is_immediate_constituent_of All x,r by QC_LANG2:63;
then r is_proper_subformula_of p by A8, QC_LANG2:83;
then r is_subformula_of p by QC_LANG2:def 22;
then ( QuantNbr r = n & QuantNbr (All x,r) = n ) by A1, A8;
then n + (- n) = (1 + n) + (- n) by CQC_SIM1:18;
hence contradiction ; :: thesis: verum

end;

hence S₁[ All x,r] ; :: thesis: verum

end;

then A9: for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for l being CQC-variable_list of
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! l] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All x,r] ) ) by A2, A5, CQC_SIM1:14, CQC_SIM1:15;
A10: for r being Element of CQC-WFF holds S₁[r] from CQC_LANG:sch 1(A9);
QuantNbr p = n by A1;
hence n = 0 by A10; :: thesis: verum