scheme :: CHAIN_1:sch 2
NonEmptyFinite{ F₁() -> non empty set , F₂() -> non empty finite Subset of F₁(), P₁[ set ] } :

P₁[F₂()]

provided

A1: for x being Element of F₁() st x in F₂() holds
P₁[{x}] and
A2: for x being Element of F₁()
for B being non empty finite Subset of F₁() st x in F₂() & B c= F₂() & not x in B & P₁[B] holds
P₁[B \/ {x}]