let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al

for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub])

defpred S_{1}[ Element of CQC-WFF Al] means for Sub being CQC_Substitution of Al holds QuantNbr $1 = QuantNbr (CQC_Sub [$1,Sub]);

A1: 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_{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 Th15, Th18, Th21, Th23, Th24;

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

for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub])

defpred S

A1: 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

thus for r being Element of CQC-WFF Al holds S