equal
deleted
inserted
replaced
369 proof (induct A) |
369 proof (induct A) |
370 case empty |
370 case empty |
371 then show ?case by simp |
371 then show ?case by simp |
372 next |
372 next |
373 case (insert a A) |
373 case (insert a A) |
374 with R show ?case |
374 have False |
375 by (metis empty_iff insert_iff) (* somewhat slow *) |
375 using R(1)[of a] R(2)[of _ a] insert(3,4) by blast |
|
376 thus ?case .. |
376 qed |
377 qed |
377 |
378 |
378 corollary Union_maximal_sets: |
379 corollary Union_maximal_sets: |
379 assumes "finite \<F>" |
380 assumes "finite \<F>" |
380 shows "\<Union>{T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} = \<Union>\<F>" |
381 shows "\<Union>{T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} = \<Union>\<F>" |