scheme :: ORDERS_5:sch 1
Finite2{ F1() -> set , F2() -> Subset of F1(), P1[ set ] } :
P1[F1()]
provided
A1: F1() is finite and
A2: P1[F2()] and
A3: for x, C being set st x in F1() \ F2() & F2() c= C & C c= F1() & P1[C] holds
P1[C \/ {x}]