scheme :: SUBSTUT1:sch 2
SubQCInd2{ F1() -> QC-alphabet , P1[ Element of QC-Sub-WFF F1()] } :
for S being Element of QC-Sub-WFF F1() holds P1[S]
provided
A1: for S being Element of QC-Sub-WFF F1() holds
( ( S is Sub_atomic implies P1[S] ) & ( S is F1() -Sub_VERUM implies P1[S] ) & ( S is Sub_negative & P1[ Sub_the_argument_of S] implies P1[S] ) & ( S is Sub_conjunctive & P1[ Sub_the_left_argument_of S] & P1[ Sub_the_right_argument_of S] implies P1[S] ) & ( S is Sub_universal & P1[ Sub_the_scope_of S] implies P1[S] ) )