let Al be QC-alphabet ; 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; ( ( 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)
; QuantNbr p = 0
defpred S1[ 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 S1[r] & S1[s] holds
S1[r '&' s]
for r being Element of CQC-WFF Al st S1[r] holds
S1[ 'not' r]
then A8:
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
( S1[ VERUM Al] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) )
by A1, A2, CQC_SIM1:14, CQC_SIM1:15;
for r being Element of CQC-WFF Al holds S1[r]
from CQC_LANG:sch 1(A8);
hence
QuantNbr p = 0
; verum