defpred S_{1}[ Element of CQC-WFF F_{1}()] means ( QuantNbr $1 = 0 implies P_{1}[$1] );

A2: for x being bound_QC-variable of F_{1}()

for p being Element of CQC-WFF F_{1}() st S_{1}[p] holds

S_{1}[ All (x,p)]
_{1}() st S_{1}[p] & S_{1}[q] holds

S_{1}[p '&' q]
_{1}()

for x being bound_QC-variable of F_{1}()

for k being Nat

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( S_{1}[ VERUM F_{1}()] & 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 A1, A2, CQC_SIM1:16;

for p being Element of CQC-WFF F_{1}() holds S_{1}[p]
from CQC_LANG:sch 1(A4);

hence for p being Element of CQC-WFF F_{1}() st QuantNbr p = 0 holds

P_{1}[p]
; :: thesis: verum

A2: for x being bound_QC-variable of F

for p being Element of CQC-WFF F

S

proof

for p, q being Element of CQC-WFF F
let x be bound_QC-variable of F_{1}(); :: thesis: for p being Element of CQC-WFF F_{1}() st S_{1}[p] holds

S_{1}[ All (x,p)]

let p be Element of CQC-WFF F_{1}(); :: thesis: ( S_{1}[p] implies S_{1}[ All (x,p)] )

assume S_{1}[p]
; :: thesis: S_{1}[ All (x,p)]

assume QuantNbr (All (x,p)) = 0 ; :: thesis: P_{1}[ All (x,p)]

then (QuantNbr p) + 1 = 0 by CQC_SIM1:18;

hence P_{1}[ All (x,p)]
; :: thesis: verum

end;S

let p be Element of CQC-WFF F

assume S

assume QuantNbr (All (x,p)) = 0 ; :: thesis: P

then (QuantNbr p) + 1 = 0 by CQC_SIM1:18;

hence P

S

proof

then A4:
for r, s being Element of CQC-WFF F
let p, q be Element of CQC-WFF F_{1}(); :: thesis: ( S_{1}[p] & S_{1}[q] implies S_{1}[p '&' q] )

assume A3: ( S_{1}[p] & S_{1}[q] )
; :: thesis: S_{1}[p '&' q]

assume QuantNbr (p '&' q) = 0 ; :: thesis: P_{1}[p '&' q]

then (QuantNbr p) + (QuantNbr q) = 0 by CQC_SIM1:17;

hence P_{1}[p '&' q]
by A1, A3; :: thesis: verum

end;assume A3: ( S

assume QuantNbr (p '&' q) = 0 ; :: thesis: P

then (QuantNbr p) + (QuantNbr q) = 0 by CQC_SIM1:17;

hence P

for x being bound_QC-variable of F

for k being Nat

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( S

for p being Element of CQC-WFF F

hence for p being Element of CQC-WFF F

P