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