scheme :: FINSET_1:sch 2
Finite{ F₁() -> set , P₁[ set ] } :

P₁[F₁()]

provided

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