scheme :: TREES_2:sch 4
FuncExOfMinNat{ P₁[ object , Nat], F₁() -> set } :

ex f being Function st
( dom f = F₁() & ( for x being object st x in F₁() holds
ex n being Nat st
( f . x = n & P₁[x,n] & ( for m being Nat st P₁[x,m] holds
n <= m ) ) ) )

provided

A1: for x being object st x in F₁() holds
ex n being Nat st P₁[x,n]