proposition: Lemma complementary_P1 : forall D:R -> Prop, ~ (exists y : R, intersection_domain D (complementary D) y).
proof: Proof. intro; red; intro; elim H; intros; unfold intersection_domain, complementary in H0; elim H0; intros; elim H2; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type