scheme :: PRE_POLY:sch 2
SubFinite{ F₁() -> set , F₂() -> Subset of F₁(), P₁[ set ] } :

P₁[F₂()]

provided

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