proposition: Lemma Setminus_Disjoint_noop: forall A s1 s2, Intersection A s1 s2 = Empty_set A -> Setminus A s1 s2 = s1.
proof: Proof. intros. apply Extensionality_Ensembles. split. * intros x H1. inversion_clear H1. intuition. * intros x H1. constructor; intuition. contradict H. apply Inhabited_not_empty. exists x. intuition. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset