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