src/HOL/Finite_Set.thy

   assume "finite T"
   with \<open>S \<subseteq> T\<close> have "finite S" by (simp add: finite_subset)
   with \<open>infinite S\<close> show False by simp
 qed
 
+corollary finite_arbitrarily_large_disj:
+  "\<lbrakk> infinite(UNIV::'a set); finite (A::'a set) \<rbrakk> \<Longrightarrow> \<exists>B. finite B \<and> card B = n \<and> A \<inter> B = {}"
+using infinite_arbitrarily_large[of "UNIV - A"]
+by fastforce
+
 proposition infinite_coinduct [consumes 1, case_names infinite]:
   assumes "X A"
     and step: "\<And>A. X A \<Longrightarrow> \<exists>x\<in>A. X (A - {x}) \<or> infinite (A - {x})"
   shows "infinite A"
 proof