scheme :: SUBSTUT2:sch 1
CQCInd1{ F1() -> QC-alphabet , P1[ set ] } :
for p being Element of CQC-WFF F1() holds P1[p]
provided
A1: for p being Element of CQC-WFF F1() st QuantNbr p = 0 holds
P1[p] and
A2: for k being Nat st ( for p being Element of CQC-WFF F1() st QuantNbr p = k holds
P1[p] ) holds
for p being Element of CQC-WFF F1() st QuantNbr p = k + 1 holds
P1[p]