Soit F[a,b] une fonctionnelle et E un ensemble bien ordonné par la relation <E. D'après l'axiome de compréhension, pour tout élément x de F(E), il existe un ensemble Ax = {a∈E | F[a,x]}. Ax est une partie non vide de E (ou sinon x ∉ F(E)) et possède un plus petit élément que l'on notera ax. F(E) est alors bien ordonné par la relation <F(E) définie ainsi : ∀(x,y)∈F(E)2, x <F(E) y ⇔ ax <E ay
Si P est une partie non vide de F(E), d'après l'axiome de compréhension, il existe un ensemble A = {a∈E | ∃p∈P, a = ap}. A est une partie non vide de E (ou sinon P est vide), donc on peut poser a = min(A). Le plus petit élément de P est alors l'élément m de P tel que F[a,m]. En effet, pour tout p ≠ m élément de P, on ap ∈ A, et par définition a = am <E ap ⇔ m <F(E) p.
Soient E un ensemble bien ordonnable et R une relation d'équivalence sur cet ensemble (réflexive, symétrique et transitive). On rappel que l'ensemble quotient E/R est l'ensemble dont les éléments sont des classes d'équivalence pour la relation R (sous-ensemble de E dont les éléments sont équivalents pour R). Cet ensemble est inclus dans ℘(E) et est donc bien ordonnable.
On peut cependant trouver un bon ordre sur E/R sans passer par l'ensemble des parties. En effet, les classes d'équivalence possèdent la particularité d'être toutes disjointes entre elles. Pour comparer ces classes d'équivalence, il suffit donc de comparer leurs minima (qui existent car une classe d'équivalence est inclus dans E). Le bon ordre sur E assure alors celui sur E/R pour la relation suivante :
Soient x et y des éléments de E/R tels que x ≤E/R y et y ≤E/R x. Alors min(x) = min(y), et donc les classes d'équivalence x et y ont un élément en commun : elles sont donc égales : x = y.
Soient x,y, z des éléments de E/R tels que x ≤E/R y et y ≤E/R z. Si x = y ou y = z, alors la transitivité est démontrée. Sinon, min(x) < min(y) et min(y) < min(z), et donc min(x) < min(z) → x ≤E/R z.
Soit m l'unique classe d'équivalence qui contienne min(E). Alors il est clair que m = min(E/R), puisque pour tout x de E/R, min(m) = min(E) <E min(x) ⇔ m <E/R x.
