--- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Wed Mar 05 18:28:57 2025 +0100
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Tue Mar 11 10:20:44 2025 +0100
@@ -51,6 +51,7 @@
 
 lemma equiv_starrel: "equiv UNIV starrel"
 proof (rule equivI)
+  show "starrel \<subseteq> UNIV \<times> UNIV" by simp
   show "refl starrel" by (simp add: refl_on_def)
   show "sym starrel" by (simp add: sym_def eq_commute)
   show "trans starrel" by (intro transI) (auto elim: eventually_elim2)