scheme :: SUBSTUT2:sch 3
CQCInd3{ F1() -> QC-alphabet , P1[ set ] } :
for p being Element of CQC-WFF F1() st QuantNbr p = 0 holds
P1[p]
provided
A1: 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
( P1[ VERUM F1()] & P1[P ! l] & ( P1[r] implies P1[ 'not' r] ) & ( P1[r] & P1[s] implies P1[r '&' s] ) )