proposition: Lemma sincl_add_x : forall (A B:Ensemble U) (x:U), ~ In U A x -> Strict_Included U (Add U A x) (Add U B x) -> Strict_Included U A B.
proof: Proof. intros A B x H' H'0; red. lapply (Strict_Included_inv U (Add U A x) (Add U B x)); auto with sets. clear H'0; intro H'0; split. - apply incl_add_x with (x := x); tauto. - elim H'0; intros H'1 H'2; elim H'2; clear H'0 H'2. intros x0 H'0. red; intro H'2. elim H'0; clear H'0. rewrite <- H'2; auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset Powerset_facts Classical Classical_sets