scheme :: PRE_CIRC:sch 5
MinValue{ F₁() -> non empty finite set , F₂( Element of F₁()) -> Real } :

ex x being Element of F₁() st
for y being Element of F₁() holds F₂(x) <= F₂(y)