fact: Definition subfamily (f:family) (D:R -> Prop) : family := mkfamily (intersection_domain (ind f) D) (fun x y:R => f x y /\ D x) (restriction_family f D).
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type