scheme :: SUBSTUT2:sch 1
CQCInd1{ 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]