proposition: Lemma incl_add_x : forall (A B:Ensemble U) (x:U), ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B.
proof: Proof. unfold Included. intros A B x H' H'0 x0 H'1. lapply (H'0 x0); auto with sets. intro H'2; lapply (Add_inv U B x x0); auto with sets. intro H'3; elim H'3; [ intro H'4; try exact H'4; clear H'3 | intro H'4; clear H'3 ]. absurd (In U A x0); auto with sets. rewrite <- H'4; auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset