scheme :: PROOFS_1:sch 3
ProofInduction{ F₁() -> set , F₂() -> Rule, P₁[ object ] } :

for a being object st F₁(),F₂() |- a holds
P₁[a]

provided

A1: for a being object st a in F₁() holds
P₁[a] and
A2: for X being set
for a being object st [X,a] in F₂() & ( for b being object st b in X holds
P₁[b] ) holds
P₁[a]