defpred S₁[ Element of CQC-WFF ] means ( QuantNbr $1 = 0 implies P₁[$1] );
A2: for x being bound_QC-variable
for p being Element of CQC-WFF st S₁[p] holds
S₁[ All (x,p)]

proof

let x be bound_QC-variable; :: thesis: for p being Element of CQC-WFF st S₁[p] holds
S₁[ All (x,p)]
let p be Element of CQC-WFF ; :: thesis: ( S₁[p] implies S₁[ All (x,p)] )
assume S₁[p] ; :: thesis: S₁[ All (x,p)]
assume QuantNbr (All (x,p)) = 0 ; :: thesis: P₁[ All (x,p)]
then (QuantNbr p) + 1 = 0 by CQC_SIM1:18;
hence P₁[ All (x,p)] ; :: thesis: verum

end;

for p, q being Element of CQC-WFF st S₁[p] & S₁[q] holds
S₁[p '&' q]

proof

let p, q be Element of CQC-WFF ; :: thesis: ( S₁[p] & S₁[q] implies S₁[p '&' q] )
assume A3: ( S₁[p] & S₁[q] ) ; :: thesis: S₁[p '&' q]
assume QuantNbr (p '&' q) = 0 ; :: thesis: P₁[p '&' q]
then (QuantNbr p) + (QuantNbr q) = 0 by CQC_SIM1:17;
hence P₁[p '&' q] by A1, A3; :: thesis: verum

end;

then A4: 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:16;
for p being Element of CQC-WFF holds S₁[p] from CQC_LANG:sch 1(A4);
hence for p being Element of CQC-WFF st QuantNbr p = 0 holds
P₁[p] ; :: thesis: verum