equal
deleted
inserted
replaced
2790 by (simp add: \<open>finite \<F>\<close>) |
2790 by (simp add: \<open>finite \<F>\<close>) |
2791 next |
2791 next |
2792 show "U ` \<F> \<subseteq> \<U>" |
2792 show "U ` \<F> \<subseteq> \<U>" |
2793 using \<open>\<F> \<subseteq> \<V>\<close> U by auto |
2793 using \<open>\<F> \<subseteq> \<V>\<close> U by auto |
2794 next |
2794 next |
2795 show "f ` S \<subseteq> UNION \<F> U" |
2795 show "f ` S \<subseteq> \<Union> (U ` \<F>)" |
2796 using \<F>(2-3) U UnionE subset_eq U by fastforce |
2796 using \<F>(2-3) U UnionE subset_eq U by fastforce |
2797 qed |
2797 qed |
2798 qed |
2798 qed |
2799 |
2799 |
2800 |
2800 |