scheme :: QC_LANG1:sch 1
QCInd{ F₁() -> QC-alphabet , P₁[ Element of QC-WFF F₁()] } :

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

provided

A1: for k being Nat
for P being QC-pred_symbol of k,F₁()
for ll being QC-variable_list of k,F₁() holds P₁[P ! ll] and
A2: P₁[ VERUM F₁()] and
A3: for p being Element of QC-WFF F₁() st P₁[p] holds
P₁[ 'not' p] and
A4: for p, q being Element of QC-WFF F₁() st P₁[p] & P₁[q] holds
P₁[p '&' q] and
A5: for x being bound_QC-variable of F₁()
for p being Element of QC-WFF F₁() st P₁[p] holds
P₁[ All (x,p)]