proposition: Lemma incl_st_add_soustr : forall (X Y:Ensemble U) (x:U), ~ In U X x -> Strict_Included U (Add U X x) Y -> Strict_Included U X (Subtract U Y x).
proof: Proof. intros X Y x H' H'0; apply sincl_add_x with (x := x); auto using add_soustr_1 with sets. split. - elim H'0. intros H'1 H'2. generalize (Inclusion_is_transitive U). intro H'4; red in H'4. apply H'4 with (y := Y); auto using add_soustr_2 with sets. - red in H'0. elim H'0; intros H'1 H'2; try exact H'1; clear H'0. red; intro H'0; apply H'2. rewrite H'0; auto 8 using add_soustr_xy, add_soustr_1, add_soustr_2 with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset Powerset_facts Classical Classical_sets