定義 Xを集合とする．

1. P₀(X) := P(X)＼{ ∅ }
2. E(X) := { {x} | x∈X }
3. F(X) := { Y⊂X | Yは有限集合 }
4. F₀(X) := F(X)＼{ ∅ }

これらは包含関係⊂により順序集合である．

定義 (X, ≦)を順序集合，Y⊂Xを部分順序とする．
写像φ: X→Y がcontractionである ⇔ 任意のx∈Xに対してφ(x)≦xとなる．

定理1 次の命題は(ZF上)同値．

1. 選択公理
2. 任意の集合Xに対して，contraction P₀(X)→E(X) が存在する．
3. 任意の集合Xに対して，contraction P₀(X)→F(X) が存在する．

証明 (1 ⇒ 2) Xを任意の集合とする．P₀(X) に選択公理を適用して 選択関数 f: P₀(X)→X を得る． このとき明らかに Y に { f(Y) } を対応させる写像はcontractionである．

(2 ⇒ 1) を非空集合の族とする． に仮定を適用してcontraction φ: P₀(X)→E(X) を得る．任意のλ∈Λに対してφ(X_λ)⊂X_λである．φ(X_λ)∈E(X)だからφ(X_λ) = { x_λ } と書ける．{ x_λ } = φ(X_λ)⊂X_λ だからx_λ∈X_λとなる．よって(x_λ)_λ∈Λ∈である．

(1 ⇔ 3) 同様にして AMC⇔3 であることが分かる．

定義 (X, ≦)を順序集合，s∈Xを部分順序Y⊂Xの上界とする．
sがYのconstructive supremumである
⇔ ある写像ψ: X→Y が存在して，任意のx∈Xに対して「s≦x ⇔ ψ(x)≦x」となる

命題 (X, ≦)を順序集合として，Y⊂Xはconstructive supremum s∈Xを持つとする． このときsはYの上限である．

証明constructive supremumの定義から，ある写像ψ: X→Y が存在して任意のx∈Xに対して「s≦x⇔ψ(x)≦x」となる．t∈XをYの上界とすると，上界の定義によりψ(t)≦tであるからs≦tとなる．よってsはYの最小上界である．

定理2 次の命題は(ZF上)同値．

1. 選択公理
2. (X, ≦)を順序集合として，Y(≠∅)⊂X は上限sを持つとする． このときsはYのconstructive supremumである．
3. (X, ≦)を完備束として，Y(≠∅)⊂X の上限をsとする． このときsはYのconstructive supremumである．
4. (X, ≦)をpowerset latticeとして，Y(≠∅)⊂X の上限をsとする． このときsはYのconstructive supremumである．

証明 (1 ⇒ 2) (X, ≦)を順序集合，s∈XをY(≠∅)⊂Xの上限とする．x∈Xに対して

s≦xのとき　A_x := Y
￢s≦xのとき　A_x := { y∈Y | ￢y≦x }

と置く．￢s≦xのとき，xはYの上界ではないからA_x≠∅である．故に集合族 { A_x }_x∈X に選択公理を適用すると選択関数 f: X→∪_x∈X A_x⊂Y を得る．この f は明らかに「s≦x ⇔ f(x)≦x」を満たす．

2⇒3 と 3⇒4 は明らか．

(4 ⇒ 1) 定理1の条件2を示す．Xを集合とする．P(X)はpowerset latticeだから，E(X)⊂P(X)の上限Xはconstructiveである．故にある写像ψ: P(X)→E(X) が存在して，任意のY⊂Xに対して「X⊂Y⇔ψ(Y)⊂Y」となる．即ち「Y ⊊ X ⇔ ￢ψ(Y)⊂Y」である．

Y∈P₀(X)に対してφ(Y) := ψ(X＼Y)∩Y と置く．X＼Y ⊊ X だから ￢ψ(X＼Y)⊂X＼Y である．故にψ(X＼Y)∩Y≠∅となる．ψ(X＼Y)∈E(X) だからψ(X＼Y)∩Y∈E(X) である．よってφは P₀(X) から E(X) への写像であるが，定義から明らかにcontractionである．

定義 順序集合(X, ≦)がconstructively directedである
⇔ある写像φ: F₀(X)→X が存在して，任意の Y∈F₀(X) に対してφ(Y)はYの上界である．(この写像φをconstructtive directionと呼ぶ)

定理3 選択公理 ⇔ 任意の有向集合はconstructively directedである．

証明 (⇒) (X, ≦)を有向集合とする．Y∈F₀(X) に対して A_Y := { x∈X | xはYの上界 } と置き { A_Y }_Y∈F0(X) に選択公理を適用すればよい．

(←) を互いに素な非空集合の族とする．Λは無限集合であるとしてよい．として G := { A∈F₀(X) | 任意のλ∈Λに対して |A∩X_λ|≦1 } と置く．G∩Λ = ∅ としてよい．このとき S := G∪Λ の順序≦を，s, t∈Sに対して

s < t
⇔ 「s, t∈Gかつ{λ∈Λ| s∩X_λ≠∅ } ⊊ {λ∈Λ| t∩X_λ≠∅ }」または「s∈Λ, t∈G かつ |t∩X_s| = 1」

で定義する．このとき(S, ≦)は有向集合である．

故に仮定によりconstructive direction φ: F₀(S)→S が存在する．λ, μ∈Λ, λ≠μとするとき明らかに |φ( {λ, μ} )∩X_λ| = 1 である．そこでμ∈Λとx_μ∈X_μを取り，λ≠μに対して φ( {λ, μ} )∩X_λ = { x_λ } と書けば ( x_λ )_λ∈Λ∈である．