diff --git a/Lebesgue/Subset_any.v b/Lebesgue/Subset_any.v
index 1b9376ff88cf6cbd7d60636fe1d3aa00bba20901..182d294b02477d2dae1b7371571c4e6c659ab5db 100644
--- a/Lebesgue/Subset_any.v
+++ b/Lebesgue/Subset_any.v
@@ -450,6 +450,14 @@ intros; rewrite inter_comm, inter_inter_any_distr_l; try easy.
 f_equal; apply functional_extensionality; intros; apply inter_comm.
 Qed.
 
+Lemma incl_inter_union_any :
+  inhabited Idx ->
+  forall (A : Idx -> U -> Prop),
+    incl (inter_any A) (union_any A).
+Proof.
+intros [i0] A x Hx; exists i0; apply (Hx i0).
+Qed.
+
 (** De Morgan's laws. *)
 
 Lemma compl_union_any :