scheme :: PCOMPS_2:sch 1
MinSet{ F₁() -> set , F₂() -> Relation, P₁[ object ] } :

ex X being set st
( X in F₁() & P₁[X] & ( for Y being set st Y in F₁() & P₁[Y] holds
[X,Y] in F₂() ) )

provided

A1: F₂() well_orders F₁() and
A2: ex X being set st
( X in F₁() & P₁[X] )