scheme :: ABCMIZ_0:sch 1
MinimalFiniteSet{ P1[ set ] } :
ex A being finite set st
( P1[A] & ( for B being set st B c= A & P1[B] holds
B = A ) )
provided
A1: ex A being finite set st P1[A]