scheme :: COHSP_1:sch 1
MinimalElementwrtIncl{ F₁() -> set , F₂() -> set , P₁[ set ] } :

ex a being set st
( a in F₂() & P₁[a] & ( for b being set st b in F₂() & P₁[b] & b c= a holds
b = a ) )

provided

A1: ( F₁() in F₂() & P₁[F₁()] ) and
A2: F₁() is finite