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