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: QuantNbr p = 0

defpred S_{1}[ 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 S_{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 A1, A2, CQC_SIM1:14, CQC_SIM1:15;

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

hence QuantNbr p = 0 ; :: thesis: verum

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: QuantNbr p = 0

defpred S

A2: for r, s being Element of CQC-WFF Al st S

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

assume A4: r '&' s is_subformula_of p ; :: thesis: QuantNbr (r '&' s) = 0

s is_immediate_constituent_of r '&' s by QC_LANG2:45;

then A5: s is_proper_subformula_of p by A4, QC_LANG2:63;

r is_immediate_constituent_of r '&' s by QC_LANG2:45;

then r is_proper_subformula_of p by A4, QC_LANG2:63;

then QuantNbr (r '&' s) = 0 + 0 by A3, A5, CQC_SIM1:17, QC_LANG2:def 21;

hence QuantNbr (r '&' s) = 0 ; :: thesis: verum

end;assume A3: ( S

assume A4: r '&' s is_subformula_of p ; :: thesis: QuantNbr (r '&' s) = 0

s is_immediate_constituent_of r '&' s by QC_LANG2:45;

then A5: s is_proper_subformula_of p by A4, QC_LANG2:63;

r is_immediate_constituent_of r '&' s by QC_LANG2:45;

then r is_proper_subformula_of p by A4, QC_LANG2:63;

then QuantNbr (r '&' s) = 0 + 0 by A3, A5, CQC_SIM1:17, QC_LANG2:def 21;

hence QuantNbr (r '&' s) = 0 ; :: thesis: verum

S

proof

then A8:
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 A6: S_{1}[r]
; :: thesis: S_{1}[ 'not' r]

A7: 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 A7, QC_LANG2:63;

hence QuantNbr ('not' r) = 0 by A6, CQC_SIM1:16, QC_LANG2:def 21; :: thesis: verum

end;assume A6: S

A7: 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 A7, QC_LANG2:63;

hence QuantNbr ('not' r) = 0 by A6, 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

for r being Element of CQC-WFF Al holds S

hence QuantNbr p = 0 ; :: thesis: verum