defpred S1[ Element of CQC-WFF F1()] means ( QuantNbr \$1 = 0 implies P1[\$1] );
A2: for x being bound_QC-variable of F1()
for p being Element of CQC-WFF F1() st S1[p] holds
S1[ All (x,p)]
proof
let x be bound_QC-variable of F1(); :: thesis: for p being Element of CQC-WFF F1() st S1[p] holds
S1[ All (x,p)]

let p be Element of CQC-WFF F1(); :: thesis: ( S1[p] implies S1[ All (x,p)] )
assume S1[p] ; :: thesis: S1[ All (x,p)]
assume QuantNbr (All (x,p)) = 0 ; :: thesis: P1[ All (x,p)]
then (QuantNbr p) + 1 = 0 by CQC_SIM1:18;
hence P1[ All (x,p)] ; :: thesis: verum
end;
for p, q being Element of CQC-WFF F1() st S1[p] & S1[q] holds
S1[p '&' q]
proof
let p, q be Element of CQC-WFF F1(); :: thesis: ( S1[p] & S1[q] implies S1[p '&' q] )
assume A3: ( S1[p] & S1[q] ) ; :: thesis: S1[p '&' q]
assume QuantNbr (p '&' q) = 0 ; :: thesis: P1[p '&' q]
then (QuantNbr p) + () = 0 by CQC_SIM1:17;
hence P1[p '&' q] by A1, A3; :: thesis: verum
end;
then A4: for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( S1[ VERUM F1()] & 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 ;
for p being Element of CQC-WFF F1() holds S1[p] from hence for p being Element of CQC-WFF F1() st QuantNbr p = 0 holds
P1[p] ; :: thesis: verum