scheme :: AOFA_000:sch 1
MaxVal{ F₁() -> non empty set , F₂() -> set , P₁[ object , object ] } :

ex n being Nat st
for x being Element of F₁() st x in F₂() holds
P₁[x,n]

provided

A1: F₂() is finite and
A2: for x being Element of F₁() st x in F₂() holds
ex n being Nat st P₁[x,n] and
A3: for x being Element of F₁()
for n, m being Nat st P₁[x,n] & n <= m holds
P₁[x,m]