scheme :: CHAIN_1:sch 3
NonTrivialFinite{ F₁() -> non trivial set , F₂() -> non trivial finite Subset of F₁(), P₁[ set ] } :

P₁[F₂()]

provided

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