scheme :: SUBSTUT2:sch 2
CQCInd2{ F₁() -> QC-alphabet , P₁[ set ] } :

for p being Element of CQC-WFF F₁() holds P₁[p]

provided

A1: for p being Element of CQC-WFF F₁() st QuantNbr p <= 0 holds
P₁[p] and
A2: for k being Nat st ( for p being Element of CQC-WFF F₁() st QuantNbr p <= k holds
P₁[p] ) holds
for p being Element of CQC-WFF F₁() st QuantNbr p <= k + 1 holds
P₁[p]