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