equal
deleted
inserted
replaced
783 from fs at4[OF at] have "infinite ((UNIV::'x set) - A)" |
783 from fs at4[OF at] have "infinite ((UNIV::'x set) - A)" |
784 by (simp add: Diff_infinite_finite) |
784 by (simp add: Diff_infinite_finite) |
785 hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:) |
785 hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:) |
786 then obtain c::"'x" where "c\<in>((UNIV::'x set) - A)" by force |
786 then obtain c::"'x" where "c\<in>((UNIV::'x set) - A)" by force |
787 then have "c\<notin>A" by simp |
787 then have "c\<notin>A" by simp |
788 then show ?thesis using prems by simp |
788 then show ?thesis .. |
789 qed |
789 qed |
790 |
790 |
791 text {* there always exists a fresh name for an object with finite support *} |
791 text {* there always exists a fresh name for an object with finite support *} |
792 lemma at_exists_fresh': |
792 lemma at_exists_fresh': |
793 fixes x :: "'a" |
793 fixes x :: "'a" |