Missed that one.

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 :