diff --git a/Lebesgue/Set_theory/Set_system/Set_system_base_finite.v b/Lebesgue/Set_theory/Set_system/Set_system_base_finite.v
index be412d473aa26cf314dc5a7994eebaab3a5e892f..53203eea2d3748b0c1fbfd188eced39300edd72e 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_base_finite.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_base_finite.v
@@ -271,7 +271,7 @@ Qed.
 Lemma Inter_finite_closure_Gen : Incl P (Inter_finite_closure P).
 Proof.
 intros A HA; replace A with (cst_seq A 0) by easy.
-rewrite <- (inter_finite_0 (cst_seq A)); easy.
+rewrite <- (inter_finite_0 (cst_seq A)); apply Ifc; easy.
 Qed.
 
 Lemma Union_finite_closure_Gen : Incl P (Union_finite_closure P).
@@ -282,7 +282,11 @@ Qed.
 
 Lemma Inter_finite_closure_Inter : Inter (Inter_finite_closure P).
 Proof.
-intros C D [A NA HA] [B NB HB]; clear C D.
+intros C D [ | A NA HA] [ | B NB HB]; clear C D.
+1,2: rewrite inter_fullset_l.
+3: rewrite inter_fullset_r.
+apply Ifc_full.
+1,2: apply Ifc; easy.
 rewrite inter_inter_finite_distr; apply Ifc.
 intros n Hn; apply append_in with (M := NB); try easy; lia.
 Qed.