fact: Definition intersection_vide_in (D:R -> Prop) (f:family) : Prop := forall x:R, (ind f x -> included (f x) D) /\ ~ (exists y : R, intersection_family f y).
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type