scheme :: ABCMIZ_A:sch 2
FiniteC{ F1() -> finite set , P1[ set ] } :
P1[F1()]
provided
A1: for A being Subset of F1() st ( for B being set st B c< A holds
P1[B] ) holds
P1[A]