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 S₁[ 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 S₁[r] holds
S₁[ All (x,r)]

proof

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

now :: thesis: not All (x,r) is_subformula_of p

assume A3: All (x,r) is_subformula_of p ; :: thesis: contradiction
r is_immediate_constituent_of All (x,r) by QC_LANG2:46;
then r is_proper_subformula_of p by A3, QC_LANG2:63;
then r is_subformula_of p by QC_LANG2:def 21;
then A4: QuantNbr r = n by A1;
QuantNbr (All (x,r)) = n by A1, A3;
then n + (- n) = (1 + n) + (- n) by A4, CQC_SIM1:18;
hence contradiction ; :: thesis: verum

end;

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

end;

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

proof

let r, s be Element of CQC-WFF Al; :: 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
s is_immediate_constituent_of r '&' s by QC_LANG2:45;
then A8: s is_proper_subformula_of p by A7, QC_LANG2:63;
r is_immediate_constituent_of r '&' s by QC_LANG2:45;
then r is_proper_subformula_of p by A7, QC_LANG2:63;
then QuantNbr (r '&' s) = 0 + 0 by A6, A8, CQC_SIM1:17, QC_LANG2:def 21;
hence QuantNbr (r '&' s) = 0 ; :: thesis: verum

end;

for r being Element of CQC-WFF Al st S₁[r] holds
S₁[ 'not' r]

proof

let r be Element of CQC-WFF Al; :: thesis: ( S₁[r] implies S₁[ 'not' r] )
assume A9: S₁[r] ; :: thesis: S₁[ 'not' r]
A10: r is_immediate_constituent_of 'not' r by QC_LANG2:43;
assume 'not' r is_subformula_of p ; :: thesis: QuantNbr ('not' r) = 0
then r is_proper_subformula_of p by A10, QC_LANG2:63;
hence QuantNbr ('not' r) = 0 by A9, CQC_SIM1:16, QC_LANG2:def 21; :: thesis: verum

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
( S₁[ VERUM Al] & 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 A5, A2, CQC_SIM1:14, CQC_SIM1:15;
A12: for r being Element of CQC-WFF Al holds S₁[r] from CQC_LANG:sch 1(A11);
QuantNbr p = n by A1;
hence n = 0 by A12; :: thesis: verum