diff --git a/Lebesgue/Set_theory/Set_system/Set_system_finite.v b/Lebesgue/Set_theory/Set_system/Set_system_finite.v
index ff0aacc1b109a1fa10c86abded53fab51c81b159..4cddfb8098060641f80dd4963d8c9f2788698137 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_finite.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_finite.v
@@ -294,11 +294,11 @@ Qed.
 Variable P : set_system U.
 
 Lemma is_Psyst_wEmpty :
-  is_Psyst P A0 -> is_Psyst (fun A => P A \/ A = emptyset) emptyset.
+  is_Psyst P A0 -> is_Psyst (add P emptyset) emptyset.
 Proof.
 intros H; rewrite Psyst_equiv in *; split.
 now right.
-now apply Inter_with_empty.
+now apply Inter_wEmpty.
 Qed.
 
 End Psyst_Facts.