Zornの補題

T₀が塔になることの証明

p∈P(X×Y), f:Z→X, g:Z→Y に対して p⁺: P(X)→P(Y), p^-: P(Y)→P(X), p^*(f,g): P(Z)→P(Z) を

p⁺(A) = ∪_x∈A{y∈Y|(x,y)∈p} (∀A∈P(X))
p^-(B) = ∪_y∈B{x∈X|(x,y)∈p} (∀B∈P(X))
p^*(f,g)(C) = {z∈C|(f(z),g(z))∈p} (∀C∈P(Z))

と定義します。

h:X→Y に対して h⁺: P(X)→P(Y), h^-: P(Y)→P(X),

h⁺(A) = ∪_x∈A{y∈Y|h(x)=y} (∀A∈P(X))
h^-(B) = ∪_y∈B{x∈X|h(x)=y} (∀B∈P(X))

と定義します。

f: P(X)→P(Y) が

f(A) = ∪_x∈Af({x}) (∀A∈P(X)) を満たすとき、f は IMG を満たす
y,z∈f({x}) ⇒ y = z (∀x∈X∀y∈Y∀z∈Y) を満たすとき、f は MAP を満たす
A≠φ ⇒ f(A)≠φ (∀A∈P(X)) を満たすとき、f は EXT を満たす

と定義します。

f,k: P(X)→P(Y), g: P(Y)→P(Z) のとき

(-f)(B) = {x∈X|f({x})∩B≠φ} (∀B∈P(Y))
(f+g)(A) = ∪_y∈f(A)g({y}) (∀A∈P(X))
(f*g)(A) = ∩_y∈f(A)g({y}) (∀A∈P(X))
(f∪k)(A) = ∪_x∈A(f({x})∪k({x})) (∀A∈P(X))
(f∩k)(A) = ∪_x∈A(f({x})∩k({x})) (∀A∈P(X))

と定義します。 f,k: P(X)→P(Y), g: P(Y)→P(Z) が IMG を満たすとすると

(f+g)(A) = g(f(A)) (∀A∈P(X))
(f∪k)(A) = f(A)∪k(A) (∀A∈P(X))

となります。

f,k: P(X)→P(Y), g: P(Y)→P(Z) のとき次のことが成り立ちます。

(f+g)+h=f+(g+h) (h: P(Z)→P(V))

	((f+g)+h)(A)
＝	{v∈V\|∃z∈Z(z∈(f+g)(A)∧v∈h({z}))}
＝	{v∈V\|∃z∈Z(∃y∈Y(y∈f(A)∧z∈g({y}))∧v∈h({z}))}
＝	{v∈V\|∃y∈Y(y∈f(A)∧∃z∈Z(z∈g({y})∧v∈h({z})))}
＝	{v∈V\|∃y∈Y(y∈f(A)∧v∈(g+h)({y}))}
＝	(f+(g+h))(A) (∀A∈P(X))

(f+g)*h⊇f+(g*h) (h: P(Z)→P(V))

	((f+g)*h)(A)
＝	{v∈V\|∀z∈Z(z∈(f+g)(A)⇒v∈h({z}))}
＝	{v∈V\|∀z∈Z(∃y∈Y(y∈f(A)∧z∈g({y}))⇒v∈h({z}))}
⊇	{v∈V\|∃y∈Y(y∈f(A)∧∀z∈Z(z∈g({y})⇒v∈h({z})))}
＝	{v∈V\|∃y∈Y(y∈f(A)∧v∈(g*h)({y}))}
＝	(f+(g*h))(A) (∀A∈P(X))

g が IMG を満たすとき (f+g)*h=f+(g*h) (h: P(Z)→P(V))

((f+g)*h)(A)

＝ {v∈V|∀z∈Z(z∈(f+g)(A)⇒v∈h({z}))}

＝ {v∈V|∀z∈Z(z∈g(f(A))⇒v∈h({z}))}

＝ (g*h)(f(A))

＝ (f+(g*h))(A) (∀A∈P(X))
f⊆k∧g⊆h⇒f+g⊆k+h (h: P(Y)→P(Z))

(f+g)(A)

＝ {z∈Z|∃y∈Y(y∈f(A)∧z∈g({y}))}

⊆ {z∈Z|∃y∈Y(y∈k(A)∧z∈h({y}))}

＝ (k+h)(A) (∀A∈P(X))
k⊆f∧g⊆h⇒f*g⊆k*h (h: P(Y)→P(Z))

(f+g)(A)

＝ {z∈Z|∀y∈Y(y∈f(A)⇒z∈g({y}))}

⊆ {z∈Z|∀y∈Y(y∈k(A)⇒z∈h({y}))}

＝ (k+h)(A) (∀A∈P(X))
f⊆k⇒-f⊆-k

(-f)(B)

＝ {x∈X|f({x})∩B≠φ}

⊆ {x∈X|k({x})∩B≠φ}

＝ (-k)(B) (∀B∈P(Y))
f が IMG を満たすとき -(-f)=f

(-(-f))(A)

＝ {y∈Y|(-f)({y})∩A≠φ}

＝ {y∈Y|∃x∈X(x∈(-f)({y})∧x∈A)}

＝ {y∈Y|∃x∈X(y∈f({x})∧x∈A)}

＝ f(A) (∀A∈P(X))
1⊆f+(-f)

((f+(-f))(A)

＝ {x∈X|f({x})∩f(A)≠φ}

⊇ A (∀A∈P(X))
(f*g)+h⊆f*(g+h) (h: P(Z)→P(V))

((f*g)+h)(A)

＝ {v∈V|∃z∈Z∀y∈Y((y∈f(A)⇒z∈g({y}))∧v∈h({z}))}

⊆ {v∈V|∀y∈Y∃z∈Z(y∈f(A)⇒(z∈g({y})∧v∈h({z})))}

＝ (f*(g+h))(A) (∀A∈P(X))

f⊆(f*g)*(-g)

	((fg)(-g))(A)
＝	{y∈Y\|∀z∈Z(z∈(f*g)(A)⇒y∈(-g)({z}))}
＝	{y∈Y\|∀z∈Z(∀v∈Y(v∈f(A)⇒z∈g({v}))⇒y∈(-g)({z}))}
⊇	{y∈Y\|∀z∈Z((y∈f(A)⇒z∈g({y}))⇒z∈({y}))}
⊇	{y∈Y\|y∈f(A)} (∀A∈P(X))

f が MAP を満たすとき (-f)+f⊆1

	((-f)+f)(B)
＝	{y∈Y\|∃x∈X(x∈(-f)(B)∧y∈f({x}))}
＝	{y∈Y\|∃x∈X(∃v∈Y(v∈f({x})∧v∈B)∧y∈f({x}))}
＝	{y∈Y\|∃x∈X(y∈B∧y∈f({x}))}
⊆	{y∈Y\|y∈B} (∀B∈P(Y))

g が MAP を満たすとき f*(g+h)=(f*g)*h (h: P(Z)→P(V))

	(f*(g+h))(A)
＝	{v∈V\|∀y∈Y(y∈f(A)⇒v∈(g+h)({y}))}
＝	{v∈V\|∀y∈Y(y∈f(A)⇒∃z∈Z(z∈g({y})∧v∈h({z})))}
＝	{v∈V\|∀y∈Y(y∈f(A)⇒∀z∈Z(z∈g({y})⇒v∈h({z})))}
＝	(f(gh))(A) (∀A∈P(X))

f*(g*h)⊆(f+g)*h (h: P(Z)→P(V))

	(f(gh))(A)
＝	{v∈V\|∀y∈Y(y∈f(A)⇒∀z∈Z(z∈g({y})⇒v∈h({z})))}
＝	{v∈V\|∀z∈Z∀y∈Y(y∈f(A)⇒(z∈g({y})⇒v∈h({z})))}
＝	{v∈V\|∀z∈Z∀y∈Y((y∈f(A)∧z∈g({y}))⇒v∈h({z}))}
⊆	{v∈V\|∀z∈Z(∃y∈Y(y∈f(A)∧z∈g({y}))⇒v∈h({z}))}
＝	{v∈V\|∀z∈Z(z∈(f+g)(A)⇒v∈h({z}))}
＝	((f+g)*h)(A) (∀A∈P(X))

f, k が IMG を満たすとき -(f∪k)=(-f)∪(-k)

	(-(f∪k))(B)
＝	{x∈X\|(f∪k)({x})∩B≠φ}
＝	{x∈X\|(f({x})∪k({x}))∩B≠φ}
＝	{x∈X\|f({x})∩B≠φ}∪{x∈X\|k({x})∩B≠φ}
＝	(-f)(B)∪(-k)(B)
＝	((-f)∪(-k))(B) (∀B∈P(Y))

(-(f∩k))({y})=((-f)∩(-k))({y}) (∀y∈Y)

	(-(f∩k))({y})
＝	{x∈X\|(f∩k)({x})∩{y}≠φ}
＝	{x∈X\|(f({x})∩k({x}))∩{y}≠φ}
＝	{x∈X\|f({x})∩{y}≠φ}∩{x∈X\|k({x})∩{y}≠φ}
＝	(-f)({y})∩(-k)({y})
＝	((-f)∩(-k))({y}) (∀y∈Y)

1*(-(f∩k))=1*((-f)∩(-k))

	(1*(-(f∩k)))(B)
＝	{x∈X\|∀y∈Y(y∈B∧x∈(-(f∩k))({y}))}
＝	{x∈X\|∀y∈Y(y∈B∧(f∩k)({x})∩{y}≠φ)}
＝	{x∈X\|∀y∈Y(y∈B∧y∈(f∩k)({x}))}
＝	{x∈X\|∀y∈Y(y∈B∧y∈(f({x})∩k({x}))}
＝	{x∈X\|∀y∈Y(y∈B∧y∈f({x})∧y∈k({x}))}
＝	{x∈X\|∀y∈Y(y∈B∧x∈(-f)({y})∧x∈(-k)({y}))}
＝	{x∈X\|∀y∈Y(y∈B∧x∈(-f)({y})∩(-k)({y}))}
＝	{x∈X\|∀y∈Y(y∈B∧x∈((-f)∩(-k))({y}))}
＝	(1*((-f)∩(-k)))(B) (∀B∈P(Y))

-(f+g)=(-g)+(-f)

	(-(f+g))(C)
＝	{x∈X\|(f+g)({x})∩C≠φ}
＝	{x∈X\|∃z∈Z(z∈(f+g)({x})∧z∈C)}
＝	{x∈X\|∃z∈Z(∃y∈Y(y∈f({x})∧z∈g({y}))∧z∈C)}
＝	{x∈X\|∃y∈Y(∃z∈Z(z∈g({y})∧z∈C)∧y∈f({x}))}
＝	{x∈X\|∃y∈Y(y∈(-g)(C)∧x∈(-f)({y}))}
＝	((-g)+(-f))(C) (∀C∈P(Z))

g が EXT を満たすとき f+(g*h)⊆f+(g+h) (h: P(Y)→P(Z))

	(f+(g*h))(A)
＝	{v∈V\|∃y∈Y(y∈f(A)∧v∈(g*h)({y}))}
＝	{v∈V\|∃y∈Y(y∈f(A)∧∀z∈Z(z∈g({y})⇒v∈h({z})))}
⊆	{v∈V\|∃y∈Y(y∈f(A)∧∃z∈Z(z∈g({y})∧v∈h({z})))}
＝	{v∈V\|∃y∈Y(y∈f(A)∧v∈(g+h)({y}))}
＝	(f+(g+h))(A) (∀A∈P(X))

g が EXT を満たすとき f*(g*h)⊆f*(g+h) (h: P(Y)→P(Z))

	(f(gh))(A)
＝	{v∈V\|∀y∈Y(y∈f(A)⇒v∈(g*h)({y}))}
＝	{v∈V\|∀y∈Y(y∈f(A)⇒∀z∈Z(z∈g({y})⇒v∈h({z})))}
⊆	{v∈V\|∀y∈Y(y∈f(A)⇒∃z∈Z(z∈g({y})∧v∈h({z})))}
＝	{v∈V\|∀y∈Y(y∈f(A)⇒v∈(g+h)({y}))}
＝	(f*(g+h))(A) (∀A∈P(X))

(f+g)∪(f+h)=f+(g∪h) (h: P(Y)→P(Z))

	((f+g)∪(f+h))(A)
＝	{z∈Z\|∃x∈X(x∈A∧(z∈(f+g)({x})∨z∈(f+h)({x})))}
＝	{z∈Z\|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧z∈g({y}))∨∃y∈Y(y∈f({x})∧z∈h({y}))))}
＝	{z∈Z\|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧(z∈g({y})∨z∈h({y}))))}
＝	{z∈Z\|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧z∈(g∪h)({y}))}
＝	{z∈Z\|∃x∈X(x∈A∧z∈(f+(g∪h))({x}))}
＝	(f+(g∪h))(A) (∀A∈P(X))

(f+g)∩(f+h)⊇f+(g∩h) (h: P(Y)→P(Z))

	((f+g)∩(f+h))(A)
＝	{z∈Z\|∃x∈X(x∈A∧(z∈(f+g)({x})∧z∈(f+h)({x})))}
＝	{z∈Z\|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧z∈g({y}))∧∃y∈Y(y∈f({x})∧z∈h({y}))))}
⊇	{z∈Z\|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧(z∈g({y})∧z∈h({y}))))}
＝	{z∈Z\|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧z∈(g∩h)({y}))}
＝	{z∈Z\|∃x∈X(x∈A∧z∈(f+(g∩h))({x}))}
＝	(f+(g∩h))(A) (∀A∈P(X))

f が MAP を満たすとき (f+g)∩(f+h)=f+(g∩h) (h: P(Y)→P(Z))

	((f+g)∩(f+h))(A)
＝	{z∈Z\|∃x∈X(x∈A∧(z∈(f+g)({x})∧z∈(f+h)({x})))}
＝	{z∈Z\|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧z∈g({y}))∧∃y∈Y(y∈f({x})∧z∈h({y}))))}
＝	{z∈Z\|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧(z∈g({y})∧z∈h({y}))))}
＝	{z∈Z\|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧z∈(g∩h)({y}))}
＝	{z∈Z\|∃x∈X(x∈A∧z∈(f+(g∩h))({x}))}
＝	(f+(g∩h))(A) (∀A∈P(X))

f, k が IMG を満たすとき 1*f⊆1*k⇒f⊆k

f(A)

＝ ∪_x∈Af({x})

＝ ∪_x∈A∩_y∈{x}f({y})

＝ ∪_x∈A(1 * f)({x})

⊆ ∪_x∈A(1 * k)({x})

＝ ∪_x∈A∩_y∈{x}k({y})

＝ ∪_x∈Ak({x})

＝ k(A) (∀A∈P(X))
{x}⊆(f*(-f)){x}

(f*(-f)){x}

＝ {v∈X|∀y∈Y(y∈f({x})⇒v∈(-f)({y}))}

＝ {v∈X|∀y∈Y(y∈f({x})⇒y∈f({v}))}

⊇ {x}
k∩h⊆(f*((-f)+k))∩h (h: P(X)→P(Y))

((f*((-f)+k))∩h)(A)

＝ ∪_x∈A((f*((-f)+k))({x})∩h({x}))

⊇ ∪_x∈A(((f*(-f))+k)({x})∩h({x}))

⊇ ∪_x∈A(k({x})∩h({x}))

＝ (k∩h)(A) (∀A∈P(X))

(f+g)∩(f*h)⊆f+(g∩h) (h: P(Y)→P(Z))

	((f+g)∩(f*h))(A)
＝	{z∈Z\|∃x∈X(x∈A∧z∈(f+g)({x})∧z∈(f*h)({x}))}
＝	{z∈Z\|∃x∈X(x∈A∧∃y∈Y(y∈f({x})∧z∈g({y}))∧∀y∈Y(y∈f({x})⇒z∈h({y})))}
⊆	{z∈Z\|∃x∈X(x∈A∧∃y∈Y(y∈f({x})∧z∈g({y})∧z∈h({y}))}
＝	((f+(g∩h))(A) (∀A∈P(X))

(f∪k)+g=(f+g)∪(k+g)

	((f∪k)+g)(A)
＝	{z∈Z\|∃y∈Y(y∈(f∪k)(A)∧z∈g({y}))}
＝	{z∈Z\|∃y∈Y(∃x∈X(x∈A∧(y∈f({x})∨y∈k({x}))∧z∈g({y})))}
＝	{z∈Z\|∃x∈X(x∈A∧∃y∈Y((y∈f({x})∨y∈k({x}))∧z∈g({y})))}
＝	{z∈Z\|∃x∈X(x∈A∧ (∃y∈Y((y∈f({x})∧z∈g({y}))∨∃y∈Y(y∈k({x}))∧z∈g({y}))))}
＝	((f+g)∪(k+g))(A) (∀A∈P(X))

(f∩k)+g⊆(f+g)∩(k+g)

	((f∩k)+g)(A)
＝	{z∈Z\|∃y∈Y(y∈(f∩k)(A)∧z∈g({y}))}
＝	{z∈Z\|∃y∈Y(∃x∈X(x∈A∧(y∈f({x})∧y∈k({x}))∧z∈g({y})))}
＝	{z∈Z\|∃x∈X(x∈A∧∃y∈Y((y∈f({x})∧y∈k({x}))∧z∈g({y})))}
⊆	{z∈Z\|∃x∈X(x∈A∧ (∃y∈Y((y∈f({x})∧z∈g({y}))∧∃y∈Y(y∈k({x}))∧z∈g({y}))))}
＝	((f+g)∩(k+g))(A) (∀A∈P(X))

e: X→P(X), u: P(X)⊇{{x}|x∈X}→X を

e(x) = {x}
u({x}) = x

と定義します。

Xを集合、G⊆P(X)、P⊆P(G)、p: P(G)→P(G)、p(H)=H∩P、 c: P(X)→P(X)、c(Y)=Y∩Gとします。 o, s: G→G を

1 ⊆ o⁺ + ⊆⁺
s⁺ ⊆ ⊆⁺
⊆⁺ ∩ (s⁺ + ⊆^-) ⊆ 1 ∪ s⁺

を満たすものとします。 j: P(P(X))→P(X) を IMG を満たし、 ξ が IMG、MAP、EXT を満たし ζ が ψ + ζ ⊆ ψ (∀ψ: P(G)→P(G)) を満たすならば

ξ + ⊆^- + ζ + j ⊆ ξ
ξ + ⊆⁺ + ζ + j ⊇ ξ または ξ + ⊆⁺ + ζ + j = Φ (Φ: P(G)→P(G), Φ(H)=φ)

を満たすものとします。

Init = o⁺: P(G)→P(G)
Suc = s⁺: P(G)→P(G)
Lim = e + ⊆^- + p + j⁺ + c: P(G)→P(G)
T₁ = ⊆^*(Init,1) = ⊆^*(o⁺,1): P(P(G))→P(P(G))
T₂ = ⊆^*(Suc,1) = ⊆^*(s⁺,1): P(P(G))→P(P(G))
T₃ = ⊆^*(Lim,1) = ⊆^*(e + ⊆^- + p + j⁺ + c, 1) : P(P(G))→P(P(G))
T_* = T₁ + T₂ + T₃ : P(P(G))→P(P(G))
ρ: P(G)→P(P(G)), ρ(X) = P(G)
τ = ρ + (T_* * u): P(G)→P(G)

と定義します。 f: P(G)→P(G) とすると次のことが成り立ちます。

f + Init ⊆ f ⇔ f + e + T₁ = f + e ⇔ (f + e + T₁) * u ⊆ f
f + Suc ⊆ f ⇔ f + e + T₂ = f + e ⇔ (f + e + T₂) * u ⊆ f
f + Lim ⊆ f ⇔ f + e + T₃ = f + e ⇔ (f + e + T₃) * u ⊆ f
f + e + T₁ = f + e, f + e + T₂ = f + e, f + e + T₃ = f + e ⇒ f + e + T_* = f + e
f + e + T_* = f + e ⇒ τ ⊆ f

τ ＝ ρ + (T_* * u) ＝ (ρ + T_*) * u ⊆ (f + e + T_*) * u ＝ (f + e) * u ＝ f

τ + e + T_* = τ + e

証明 (i) τ + e + T₁ = τ + e

(T₁ * u) + Init ⊆ T₁ * (u + Init) ＝ T₁ * (T₁ + u + Init) ⊆ T₁ * (T₁ + u) ＝ T₁ * u

τ + Init ＝ ρ + (T_* * u) + Init ＝ ρ + ((T_* + T₁) * u) + Init ＝ ρ + T_* + (T₁ * u) + Init

⊆ ρ + T_* + (T₁ * u) ＝ ρ + (T_* + T₁) * u ＝ ρ + (T_* * u) ＝ τ

(ii) τ + e + T₂ = τ + e

(T₂ * u) + Suc ⊆ T₂ * (u + Suc) ＝ T₂ * (T₂ + u + Suc) ⊆ T₂ * (T₂ + u) ＝ T₂ * u

τ + Suc ＝ ρ + (T_* * u) + Suc ＝ ρ + ((T_* + T₂) * u) + Suc ＝ ρ + T_* + (T₂ * u) + Suc

⊆ ρ + T_* + (T₂ * u) ＝ ρ + (T_* + T₂) * u ＝ ρ + (T_* * u) ＝ τ

(iii) τ + e + T₃ = τ + e

(T₃ * u) + Lim ⊆ T₃ * (u + Suc) ＝ T₃ * (T₃ + u + Lim) ⊆ T₃ * (T₃ + u) ＝ T₃ * u

τ + Lim ＝ ρ + (T_* * u) + Lim ＝ ρ + ((T_* + T₃) * u) + Lim ＝ ρ + T_* + (T₃ * u) + Lim

⊆ ρ + T_* + (T₃ * u) ＝ ρ + (T_* + T₃) * u ＝ ρ + (T_* * u) ＝ τ

T₀が鎖になることの証明

次のように定義します。

β = ⊆^- ∪ (Suc + ⊆⁺): P(G)→P(G)
γ = ⊆^- ∪ ⊆⁺: P(G)→P(G)
α = (⊆^- + Suc) ∩ ⊆⁺: P(G)→P(G)

次のことが成り立ちます。

α ⊆ β

	1
⊆	(1 * α) * (-α)
＝	(1 * α) * (-((⊆^- + s⁺) ∩ ⊆⁺))
＝	(1 * α) * ((-(⊆^- + s⁺)) ∩ (-⊆⁺))
＝	(1 * α) * ((s^- + ⊆⁺) ∩ ⊆^-)
⊆	(1 * α) * ((s^- + ⊆⁺) ∩ (s^- * (s⁺ + ⊆^-)))
⊆	(1 * α) * (s^- + (⊆⁺ ∩ (s⁺ + ⊆^-)))
⊆	(1 * α) * (s^- + (1 ∪ s⁺))
＝	(1 * α) * (s^- ∪ (s^- + s⁺))
＝	(1 * α) * (s^- ∪ 1)
	(1 * α)
⊆	((1 * α) * (1 ∪ s^-)) * (-(1 ∪ s^-))
⊆	1 * (-(1 ∪ s^-))
＝	1 * (1 ∪ s⁺)
	α ⊆ 1 ∪ s⁺ ⊆ β

ξ、η が IMG、MAP、EXT を満たすならば ((ξ + ⊆^-) ∪ (η + ⊆⁺)) + Lim ⊆ (ξ + ⊆^-) ∪ (η + ⊆⁺) (∀ξ,η: P(G)→P(G))

	ζ が ψ + ζ ⊆ ψ (∀ψ: P(G)→P(G))を満たすならば
	((ξ + ⊆^-) ∪ (η + ⊆⁺)) + ζ + j
＝	(ξ + ⊆^- + ζ + j) ∪ (η + ⊆⁺ + ζ + j) ⊆ ξ または ⊇ η
	((ξ + ⊆^-) ∪ (η + ⊆⁺)) + Lim
＝	((ξ + ⊆^-) ∪ (η + ⊆⁺)) + e + ⊆^- + p + + j⁺ + c
⊆	(ξ + ⊆^-) ∪ (η + ⊆⁺)

β ⊆ Suc + γ

	β
＝	⊆^- ∪ (s⁺ + ⊆⁺)
⊆	(s⁺ + s^- + ⊆^-) ∪ (s⁺ + ⊆⁺)
＝	s⁺ + ((s^- + ⊆^-) ∪ ⊆⁺)
＝	s⁺ + ((-(-⊆^- + -s^-)) ∪ ⊆⁺)
＝	s⁺ + ((-(⊆⁺ + s⁺)) ∪ ⊆⁺)
⊆	s⁺ + ((-(⊆⁺ + ⊆⁺)) ∪ ⊆⁺)
⊆	s⁺ + ((-⊆⁺) ∪ ⊆⁺)
⊆	s⁺ + (⊆^- ∪ ⊆⁺)
＝	Suc + γ

-γ = γ

-γ = -(⊆^- ∪ ⊆⁺) = (-⊆^-) ∪ (-⊆⁺) = ⊆⁺ ∪ ⊆^- = γ

(τ * γ) * τ ⊆ (τ * γ) * γ

	A∈P(G), (τ * γ)(A)≠φ のとき
	((τ * γ) * τ)(A)
＝	∩_{y∈(τ * γ)(A)}τ({y})
＝	∩_{y∈(τ * γ)(A)}τ(A)
＝	τ(A)
⊆	((τ * γ) * (-γ))(A)
＝	((τ * γ) * γ)(A)
	A∈P(G), (τ * γ)(A)＝φ のとき
	((τ * γ) * τ)(A)
＝	∩_y∈φτ({y})
＝	∩_y∈φγ({y})
＝	((τ * γ) * γ)(A)

τ ⊆ (τ * γ) * β

証明 (i) ((τ * γ) * (β ∩ τ)) + e + T₁ = ((τ * γ) * (β ∩ τ)) + e

β + Init ⊆ ⊆^- ⊆ β

(β ∩ τ) + Init ⊆ β + Init ⊆ β

(β ∩ τ) + Init ⊆ τ + Init ⊆ τ

(β ∩ τ) + Init ⊆ β ∩ τ

((τ * γ) * (β ∩ τ)) + Init ⊆ (τ * γ) * (β ∩ τ)

(ii) ((τ * γ) * (β ∩ τ)) + e + T₂ = ((τ * γ) * (β ∩ τ)) + e

	β + Suc
=	(⊆^- ∪ (Suc + ⊆⁺)) + Suc
⊆	(⊆^- + Suc) ∪ (Suc + ⊆⁺ + Suc)
⊆	(⊆^- + Suc) ∪ (Suc + ⊆⁺ + ⊆⁺)
⊆	(⊆^- + Suc) ∪ (Suc + ⊆⁺)
	((τ * γ) * (β ∩ τ)) + Suc
⊆	(τ * γ) * ((β ∩ τ) + Suc)
⊆	(τ * γ) * ((β + Suc) ∩ (τ + Suc))
⊆	(τ * γ) * (((⊆^- + Suc) ∪ (Suc + ⊆⁺)) ∩ τ)
⊆	(τ * γ) * (((⊆^- + Suc) ∪ (Suc + ⊆⁺)) ∩ γ ∩ τ)
⊆	(τ * γ) * (((⊆^- + Suc) ∪ (Suc + ⊆⁺)) ∩ (⊆^- ∪ ⊆⁺) ∩ τ)
⊆	(τ * γ) * ((⊆^- ∪ ((⊆^- + Suc) ∩ ⊆⁺) ∪ (Suc + ⊆⁺)) ∩ τ)
⊆	(τ * γ) * (β ∩ τ)

(iii) ((τ * γ) * (β ∩ τ)) + e + T₃ = ((τ * γ) * (β ∩ τ)) + e

β + Lim

= (⊆^- ∪ (Suc + ⊆⁺)) + Lim

⊆ ⊆^- ∪ (Suc + ⊆⁺)

= β

(β ∩ τ) + Lim ⊆ β + Lim ⊆ β

(β ∩ τ) + Lim ⊆ τ + Lim ⊆ τ

(β ∩ τ) + Lim ⊆ β ∩ τ

((τ * γ) * (β ∩ τ)) + Lim ⊆ (τ * γ) * (β ∩ τ)

τ ⊆ τ * γ

証明 (i) (τ * γ) + e + T₁ ⊆ (τ * γ) + e

γ + Init ⊆ ⊆^- ⊆ γ

τ * (γ + Init) ⊆ τ * γ

(τ * γ) + Init ⊆ τ * γ

(ii) (τ * γ) + e + T₂ ⊆ (τ * γ) + e

τ ⊆ (τ * γ) * β ⊆ (τ * γ) * (Suc + γ) ⊆ ((τ * γ) + Suc) * γ

(τ * γ) + Suc ⊆ (((τ * γ) + Suc) * γ) * γ ⊆ τ * γ

(iii) (τ * γ) + e + T₂ ⊆ (τ * γ) + e

γ + Lim

= (⊆^- ∪ ⊆⁺) + Lim

⊆ ⊆^- ∪ ⊆⁺

= γ

τ * (γ + Lim) ⊆ τ * γ

(τ * γ) + Lim ⊆ τ * γ

	((fg)(-g))(A)
＝	{y∈Y\|∀z∈Z(z∈(f*g)(A)⇒y∈(-g)({z}))}
＝	{y∈Y\|∀z∈Z(∀v∈Y(v∈f(A)⇒z∈g({v}))⇒y∈(-g)({z}))}
⊇	{y∈Y\|∀z∈Z((y∈f(A)⇒z∈g({y}))⇒z∈({y}))}
⊇	{y∈Y\|y∈f(A)} (∀A∈P(X))

	((f+g)*h)(A)
＝	{v∈V\|∀z∈Z(z∈(f+g)(A)⇒v∈h({z}))}
＝	{v∈V\|∀z∈Z(z∈g(f(A))⇒v∈h({z}))}
＝	(g*h)(f(A))
＝	(f+(g*h))(A) (∀A∈P(X))

	(f+g)(A)
＝	{z∈Z\|∃y∈Y(y∈f(A)∧z∈g({y}))}
⊆	{z∈Z\|∃y∈Y(y∈k(A)∧z∈h({y}))}
＝	(k+h)(A) (∀A∈P(X))

	(f+g)(A)
＝	{z∈Z\|∀y∈Y(y∈f(A)⇒z∈g({y}))}
⊆	{z∈Z\|∀y∈Y(y∈k(A)⇒z∈h({y}))}
＝	(k+h)(A) (∀A∈P(X))

	(-f)(B)
＝	{x∈X\|f({x})∩B≠φ}
⊆	{x∈X\|k({x})∩B≠φ}
＝	(-k)(B) (∀B∈P(Y))

	(-(-f))(A)
＝	{y∈Y\|(-f)({y})∩A≠φ}
＝	{y∈Y\|∃x∈X(x∈(-f)({y})∧x∈A)}
＝	{y∈Y\|∃x∈X(y∈f({x})∧x∈A)}
＝	f(A) (∀A∈P(X))

	((f*g)+h)(A)
＝	{v∈V\|∃z∈Z∀y∈Y((y∈f(A)⇒z∈g({y}))∧v∈h({z}))}
⊆	{v∈V\|∀y∈Y∃z∈Z(y∈f(A)⇒(z∈g({y})∧v∈h({z})))}
＝	(f*(g+h))(A) (∀A∈P(X))

	f(A)
＝	∪_x∈Af({x})
＝	∪_x∈A∩_y∈{x}f({y})
＝	∪_x∈A(1 * f)({x})
⊆	∪_x∈A(1 * k)({x})
＝	∪_x∈A∩_y∈{x}k({y})
＝	∪_x∈Ak({x})
＝	k(A) (∀A∈P(X))

	(f*(-f)){x}
＝	{v∈X\|∀y∈Y(y∈f({x})⇒v∈(-f)({y}))}
＝	{v∈X\|∀y∈Y(y∈f({x})⇒y∈f({v}))}
⊇	{x}

	((f*((-f)+k))∩h)(A)
＝	∪_x∈A((f*((-f)+k))({x})∩h({x}))
⊇	∪_x∈A(((f*(-f))+k)({x})∩h({x}))
⊇	∪_x∈A(k({x})∩h({x}))
＝	(k∩h)(A) (∀A∈P(X))

	(T₁ * u) + Init ⊆ T₁ * (u + Init) ＝ T₁ * (T₁ + u + Init) ⊆ T₁ * (T₁ + u) ＝ T₁ * u
	τ + Init ＝ ρ + (T_* * u) + Init ＝ ρ + ((T_* + T₁) * u) + Init ＝ ρ + T_* + (T₁ * u) + Init
⊆	ρ + T_* + (T₁ * u) ＝ ρ + (T_* + T₁) * u ＝ ρ + (T_* * u) ＝ τ

	(T₂ * u) + Suc ⊆ T₂ * (u + Suc) ＝ T₂ * (T₂ + u + Suc) ⊆ T₂ * (T₂ + u) ＝ T₂ * u
	τ + Suc ＝ ρ + (T_* * u) + Suc ＝ ρ + ((T_* + T₂) * u) + Suc ＝ ρ + T_* + (T₂ * u) + Suc
⊆	ρ + T_* + (T₂ * u) ＝ ρ + (T_* + T₂) * u ＝ ρ + (T_* * u) ＝ τ

	(T₃ * u) + Lim ⊆ T₃ * (u + Suc) ＝ T₃ * (T₃ + u + Lim) ⊆ T₃ * (T₃ + u) ＝ T₃ * u
	τ + Lim ＝ ρ + (T_* * u) + Lim ＝ ρ + ((T_* + T₃) * u) + Lim ＝ ρ + T_* + (T₃ * u) + Lim
⊆	ρ + T_* + (T₃ * u) ＝ ρ + (T_* + T₃) * u ＝ ρ + (T_* * u) ＝ τ

	β + Init ⊆ ⊆^- ⊆ β
	(β ∩ τ) + Init ⊆ β + Init ⊆ β
	(β ∩ τ) + Init ⊆ τ + Init ⊆ τ
	(β ∩ τ) + Init ⊆ β ∩ τ
	((τ * γ) * (β ∩ τ)) + Init ⊆ (τ * γ) * (β ∩ τ)

	β + Lim
=	(⊆^- ∪ (Suc + ⊆⁺)) + Lim
⊆	⊆^- ∪ (Suc + ⊆⁺)
=	β
	(β ∩ τ) + Lim ⊆ β + Lim ⊆ β
	(β ∩ τ) + Lim ⊆ τ + Lim ⊆ τ
	(β ∩ τ) + Lim ⊆ β ∩ τ
	((τ * γ) * (β ∩ τ)) + Lim ⊆ (τ * γ) * (β ∩ τ)

	γ + Init ⊆ ⊆^- ⊆ γ
	τ * (γ + Init) ⊆ τ * γ
	(τ * γ) + Init ⊆ τ * γ

	τ ⊆ (τ * γ) * β ⊆ (τ * γ) * (Suc + γ) ⊆ ((τ * γ) + Suc) * γ
	(τ * γ) + Suc ⊆ (((τ * γ) + Suc) * γ) * γ ⊆ τ * γ

	γ + Lim
=	(⊆^- ∪ ⊆⁺) + Lim
⊆	⊆^- ∪ ⊆⁺
=	γ
	τ * (γ + Lim) ⊆ τ * γ
	(τ * γ) + Lim ⊆ τ * γ

Zornの補題

T0が塔になることの証明

τ + e + T* = τ + e

T0が鎖になることの証明

τ ⊆ (τ * γ) * β

τ ⊆ τ * γ

T₀が塔になることの証明

τ + e + T_* = τ + e

T₀が鎖になることの証明