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

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

provided

A1: for p being Element of QC-WFF F₁() holds
( ( p is atomic implies P₁[p] ) & P₁[ VERUM F₁()] & ( p is negative & P₁[ the_argument_of p] implies P₁[p] ) & ( p is conjunctive & P₁[ the_left_argument_of p] & P₁[ the_right_argument_of p] implies P₁[p] ) & ( p is universal & P₁[ the_scope_of p] implies P₁[p] ) )