proposition: Lemma open_set_P2 : forall D1 D2:R -> Prop, open_set D1 -> open_set D2 -> open_set (union_domain D1 D2).
proof: Proof. unfold open_set; intros; unfold union_domain in H1; elim H1; intro. - apply neighbourhood_P1 with D1. + unfold included, union_domain; tauto. + apply H; assumption. - apply neighbourhood_P1 with D2. + unfold included, union_domain; tauto. + apply H0; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type