diff --git a/Lebesgue/Set_theory/Set_system/Set_system_base_any.v b/Lebesgue/Set_theory/Set_system/Set_system_base_any.v
index 7eb6f1b1fc1ad8e652e224c2072171663229803c..9977d75f915a51971a7f488a77ee196c3fbab5e5 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_base_any.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_base_any.v
@@ -175,6 +175,20 @@ Section Any_Facts2.
 
 Context {U : Type}.
 
+Lemma Inter_any_closure_monot :
+  forall (P1 P2 : set_system U),
+    Incl P1 P2 -> Incl (Inter_any_closure P1) (Inter_any_closure P2).
+Proof.
+intros P1 P2 HP A [Q1 HQ1]; apply Iac, Incl_trans with P1; easy.
+Qed.
+
+Lemma Union_any_closure_monot :
+  forall (P1 P2 : set_system U),
+    Incl P1 P2 -> Incl (Union_any_closure P1) (Union_any_closure P2).
+Proof.
+intros P1 P2 HP A [Q1 HQ1]; apply Uac, Incl_trans with P1; easy.
+Qed.
+
 Lemma Inter_any_closure_complp_any_eq :
   forall (P : set_system U),
     Inter_any_closure (complp_any P) = complp_any (Union_any_closure P).