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₁[ 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₁[ VERUM Al] & 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 Th15, Th18, Th21, Th23, Th24;
thus for r being Element of CQC-WFF Al holds S₁[r] from CQC_LANG:sch 1(A1); :: thesis: verum