proposition: Lemma Disjoint_Intersection: forall A s1 s2, Disjoint A s1 s2 -> Intersection A s1 s2 = Empty_set A.
proof: Proof. intros. apply Extensionality_Ensembles. split. * destruct H. intros x H1. unfold In in *. exfalso. intuition. apply (H _ H1). * intuition. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset