src/ZF/UNITY/Constrains.thy

--- a/src/ZF/UNITY/Constrains.thy	Tue Sep 27 16:51:35 2022 +0100
+++ b/src/ZF/UNITY/Constrains.thy	Tue Sep 27 17:03:23 2022 +0100
@@ -344,7 +344,7 @@
 apply (frule Stable_type [THEN subsetD], auto)
 done
 
-lemma AlwaysD: "F \<in> Always(A) \<Longrightarrow> Init(F)<=A & F \<in> Stable(A)"
+lemma AlwaysD: "F \<in> Always(A) \<Longrightarrow> Init(F)<=A \<and> F \<in> Stable(A)"
 by (simp add: Always_def initially_def)
 
 lemmas AlwaysE = AlwaysD [THEN conjE]