proposition: Lemma add_soustr_1 : forall (X:Ensemble U) (x:U), In U X x -> Included U (Add U (Subtract U X x) x) X.
proof: Proof. intros X x H'; red. intros x0 H'0; elim H'0; auto with sets. - intros y H'1; elim H'1; auto with sets. - intros t H'1; try assumption. rewrite <- (Singleton_inv U x t); auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset Powerset_facts Classical Classical_sets