proposition: Lemma restriction_family : forall (f:family) (D:R -> Prop) (x:R), (exists y : R, (fun z1 z2:R => f z1 z2 /\ D z1) x y) -> intersection_domain (ind f) D x.
proof: Proof. intros; elim H; intros; unfold intersection_domain; elim H0; intros; split. - apply (cond_fam f0); exists x0; assumption. - assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type