29 fix c assume "c \<in> chain S" |
29 fix c assume "c \<in> chain S" |
30 show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" |
30 show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" |
31 proof cases |
31 proof cases |
32 |
32 |
33 txt {* If @{text c} is an empty chain, then every element in |
33 txt {* If @{text c} is an empty chain, then every element in |
34 @{text S} is an upper bound of @{text c}. *} |
34 @{text S} is an upper bound of @{text c}. *} |
35 |
35 |
36 assume "c = {}" |
36 assume "c = {}" |
37 with aS show ?thesis by fast |
37 with aS show ?thesis by fast |
38 |
38 |
39 txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper |
39 txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper |
40 bound of @{text c}, lying in @{text S}. *} |
40 bound of @{text c}, lying in @{text S}. *} |
41 |
41 |
42 next |
42 next |
43 assume "c \<noteq> {}" |
43 assume "c \<noteq> {}" |
44 show ?thesis |
44 show ?thesis |
45 proof |
45 proof |
46 show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast |
46 show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast |
47 show "\<Union>c \<in> S" |
47 show "\<Union>c \<in> S" |
48 proof (rule r) |
48 proof (rule r) |
49 from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast |
49 from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast |
50 show "c \<in> chain S" by fact |
50 show "c \<in> chain S" by fact |
51 qed |
51 qed |
52 qed |
52 qed |
53 qed |
53 qed |
54 qed |
54 qed |
55 qed |
55 qed |