scheme :: ORDERS_5:sch 1
Finite2{ F₁() -> set , F₂() -> Subset of F₁(), P₁[ set ] } :

P₁[F₁()]

provided

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