[STATEMENT]
lemma infinite_complement_partition_finite [simp]:
  "finite (UNIV :: 'a set) \<Longrightarrow> infinite_complement_partition = (UNIV :: 'a set set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite UNIV \<Longrightarrow> infinite_complement_partition = UNIV
[PROOF STEP]
by(auto intro: finite_subset finite_complement_partition)