equal
deleted
inserted
replaced
42 done |
42 done |
43 |
43 |
44 lemma subcls1_def2: |
44 lemma subcls1_def2: |
45 "subcls1 G = |
45 "subcls1 G = |
46 (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})" |
46 (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})" |
47 by (auto simp add: is_class_def not_None_eq dest: subcls1D intro: subcls1I) |
47 by (auto simp add: is_class_def dest: subcls1D intro: subcls1I) |
48 |
48 |
49 lemma finite_subcls1: "finite (subcls1 G)" |
49 lemma finite_subcls1: "finite (subcls1 G)" |
50 apply(subst subcls1_def2) |
50 apply(subst subcls1_def2) |
51 apply(rule finite_SigmaI [OF finite_is_class]) |
51 apply(rule finite_SigmaI [OF finite_is_class]) |
52 apply(rule_tac B = "{fst (the (class G C))}" in finite_subset) |
52 apply(rule_tac B = "{fst (the (class G C))}" in finite_subset) |