--- a/src/HOL/ZF/Games.thy	Wed Mar 05 18:28:57 2025 +0100
+++ b/src/HOL/ZF/Games.thy	Tue Mar 11 10:20:44 2025 +0100
@@ -816,6 +816,9 @@
 
 lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
 proof (rule equivI)
+  show "eq_game_rel \<subseteq> UNIV \<times> UNIV"
+    by simp
+next
   show "refl eq_game_rel"
     by (auto simp only: eq_game_rel_def intro: reflI eq_game_refl)
 next