25 proof (rule Zorn_Lemma2) |
25 proof (rule Zorn_Lemma2) |
26 show "\<forall>c \<in> chains S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" |
26 show "\<forall>c \<in> chains S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" |
27 proof |
27 proof |
28 fix c assume "c \<in> chains S" |
28 fix c assume "c \<in> chains S" |
29 show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" |
29 show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" |
30 proof cases |
30 proof (cases "c = {}") |
31 txt \<open>If \<open>c\<close> is an empty chain, then every element in \<open>S\<close> is an upper |
31 txt \<open>If \<open>c\<close> is an empty chain, then every element in \<open>S\<close> is an upper |
32 bound of \<open>c\<close>.\<close> |
32 bound of \<open>c\<close>.\<close> |
33 |
33 case True |
34 assume "c = {}" |
|
35 with aS show ?thesis by fast |
34 with aS show ?thesis by fast |
36 |
35 next |
37 txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper bound of \<open>c\<close>, lying in |
36 txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper bound of \<open>c\<close>, lying in |
38 \<open>S\<close>.\<close> |
37 \<open>S\<close>.\<close> |
39 next |
38 case False |
40 assume "c \<noteq> {}" |
|
41 show ?thesis |
39 show ?thesis |
42 proof |
40 proof |
43 show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast |
41 show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast |
44 show "\<Union>c \<in> S" |
42 show "\<Union>c \<in> S" |
45 proof (rule r) |
43 proof (rule r) |