proposition: Lemma incl_soustr_add_l : forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X.
proof: Proof. intros X x; red. intros x0 H'; elim H'; auto with sets. intro H'0; elim H'0; auto with sets. intros t H'1 H'2; elim H'2; auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset Powerset_facts Classical Classical_sets