let p be Element of CQC-WFF ; :: thesis: ( ( for q being Element of CQC-WFF st q is_subformula_of p holds
for x being bound_QC-variable
for r being Element of CQC-WFF holds q <> All (x,r) ) implies QuantNbr p = 0 )
assume A1: for q being Element of CQC-WFF st q is_subformula_of p holds
for x being bound_QC-variable
for r being Element of CQC-WFF holds q <> All (x,r) ; :: thesis: QuantNbr p = 0
defpred S₁[ Element of CQC-WFF ] means ( $1 is_subformula_of p implies QuantNbr $1 = 0 );
A2: 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 A3: ( S₁[r] & S₁[s] ) ; :: thesis: S₁[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;

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 A6: S₁[r] ; :: thesis: S₁[ '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;

then A8: 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 k
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 A1, A2, CQC_SIM1:14, CQC_SIM1:15;
for r being Element of CQC-WFF holds S₁[r] from CQC_LANG:sch 1(A8);
hence QuantNbr p = 0 ; :: thesis: verum