proposition: Theorem Non_disjoint_union : forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X.
proof: Proof. intros X x H'; unfold Add. apply Extensionality_Ensembles; red. split; red; auto with sets. intros x0 H'0; elim H'0; auto with sets. intros t H'1; elim H'1; auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset