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_{1}[ 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_{1}[r] holds

S_{1}[ All (x,r)]
_{1}[r] & S_{1}[s] holds

S_{1}[r '&' s]
_{1}[r] holds

S_{1}[ 'not' r]

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_{1}[ VERUM Al] & S_{1}[P ! l] & ( S_{1}[r] implies S_{1}[ 'not' r] ) & ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] ) & ( S_{1}[r] implies S_{1}[ All (x,r)] ) )
by A5, A2, CQC_SIM1:14, CQC_SIM1:15;

A12: for r being Element of CQC-WFF Al holds S_{1}[r]
from CQC_LANG:sch 1(A11);

QuantNbr p = n by A1;

hence n = 0 by A12; :: thesis: verum

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

A2: for x being bound_QC-variable of Al

for r being Element of CQC-WFF Al st S

S

proof

A5:
for r, s being Element of CQC-WFF Al st S
let x be bound_QC-variable of Al; :: thesis: for r being Element of CQC-WFF Al st S_{1}[r] holds

S_{1}[ All (x,r)]

let r be Element of CQC-WFF Al; :: thesis: ( S_{1}[r] implies S_{1}[ All (x,r)] )

assume S_{1}[r]
; :: thesis: S_{1}[ All (x,r)]

_{1}[ All (x,r)]
; :: thesis: verum

end;S

let r be Element of CQC-WFF Al; :: thesis: ( S

assume S

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

hence
Sassume 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;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

S

proof

for r being Element of CQC-WFF Al st S
let r, s be Element of CQC-WFF Al; :: thesis: ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] )

assume A6: ( S_{1}[r] & S_{1}[s] )
; :: thesis: S_{1}[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;assume A6: ( 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

S

proof

then A11:
for r, s being Element of CQC-WFF Al
let r be Element of CQC-WFF Al; :: thesis: ( S_{1}[r] implies S_{1}[ 'not' r] )

assume A9: S_{1}[r]
; :: thesis: S_{1}[ '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;assume A9: S

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

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

A12: for r being Element of CQC-WFF Al holds S

QuantNbr p = n by A1;

hence n = 0 by A12; :: thesis: verum