equal
deleted
inserted
replaced
|
1 |
|
2 theory Zorn_Lemma = Zorn:; |
|
3 |
|
4 |
|
5 lemma Zorn's_Lemma: "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> |
|
6 EX y: S. ALL z: S. y <= z --> y = z"; |
|
7 proof (rule Zorn_Lemma2); |
|
8 assume aS: "a:S"; |
|
9 assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S"; |
|
10 show "ALL c:chain S. EX y:S. ALL z:c. z <= y"; |
|
11 proof; |
|
12 fix c; assume "c:chain S"; |
|
13 have s: "EX x. x:c ==> Union c : S"; |
|
14 by (rule r); |
|
15 show "EX y:S. ALL z:c. z <= y"; |
|
16 proof (rule case [of "c={}"]); |
|
17 assume "c={}"; |
|
18 show ?thesis; by fast; |
|
19 next; |
|
20 assume "c~={}"; |
|
21 show ?thesis; |
|
22 proof; |
|
23 have "EX x. x:c"; by fast; |
|
24 thus "Union c : S"; by (rule s); |
|
25 show "ALL z:c. z <= Union c"; by fast; |
|
26 qed; |
|
27 qed; |
|
28 qed; |
|
29 qed; |
|
30 |
|
31 |
|
32 |
|
33 end; |