diff --git a/theories/sets.v b/theories/sets.v
index 89a799b654eaa4367f1361ee809386679b64b85c..8e95e8d45f9acdef9a8c80c2f8d81691f29da107 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1145,6 +1145,11 @@ Section more_finite.
   Proof. intros Hinf [xs ?] xs'. destruct (Hinf (xs ++ xs')). set_solver. Qed.
 End more_finite.
 
+Lemma top_infinite `{TopSet A C, Infinite A} : set_infinite (⊤ : C).
+Proof.
+  intros xs. exists (fresh xs). split; [set_solver|]. apply infinite_is_fresh.
+Qed.
+
 (** Sets of sequences of natural numbers *)
 (* The set [seq_seq start len] of natural numbers contains the sequence
 [start, start + 1, ..., start + (len-1)]. *)