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

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

provided

A1: for r, s being Element of CQC-WFF F₁()
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₁() holds
( P₁[ VERUM F₁()] & P₁[P ! l] & ( P₁[r] implies P₁[ 'not' r] ) & ( P₁[r] & P₁[s] implies P₁[r '&' s] ) )