Add Union_any_inter_equiv.

Lebesgue/Set_theory/Set_system/Set_system_base_any.v

@@ -28,6 +28,30 @@ Section Any_Facts1.
 Context {U : Type}.
 Variable P : set_system U.
 
+Lemma Union_any_inter_equiv :
+  Union_any_inter P <->
+  forall A B x, P A -> P B -> inter A B x ->
+    exists C, P C /\ incl C (inter A B) /\ C x.
+Proof.
+split.
+(* *)
+intros HP A B x HA HB Hx; destruct (HP _ _ HA HB) as [Q [HQ1 HQ2]].
+rewrite HQ2 in Hx; destruct Hx as [C [HC Hx]]; exists C.
+split; auto; split; try easy; rewrite HQ2; apply unionp_any_ub; easy.
+(* *)
+intros HP A B HA HB.
+destruct (choice
+    (fun (i : { x | inter A B x}) C =>
+      P C /\ incl C (inter A B) /\ C (proj1_sig i))) as [fQ HfQ].
+  intros [x Hx]; destruct (HP _ _ _ HA HB Hx) as [C HC]; exists C; easy.
+exists (unskolem fQ); split.
+intros C [i]; apply HfQ.
+rewrite <- unionf_any_unionp_any_eq.
+apply set_ext_equiv; split; intros x Hx.
+exists (exist _ _ Hx); apply HfQ.
+destruct Hx as [i Hx], (HfQ i) as [HfQ1 [HfQ2 HfQ3]]; auto.
+Qed.
+
 Lemma Interf_any_Inter :
   Interf_any P -> Inter P.
 Proof.