equal
deleted
inserted
replaced
61 then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by fast |
61 then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by fast |
62 hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def) |
62 hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def) |
63 (* *) |
63 (* *) |
64 fix a assume *: "a \<in> Field r" |
64 fix a assume *: "a \<in> Field r" |
65 obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a" |
65 obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a" |
66 using * 1 by blast |
66 using * 1 by auto |
67 hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT |
67 hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT |
68 by (simp add: total_on_def) |
68 by (simp add: total_on_def) |
69 thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast |
69 thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast |
70 qed |
70 qed |
71 |
71 |