proposition: Lemma Intersection_Empty_set_r: forall A s, Intersection A s (Empty_set A) = Empty_set A.
proof: Proof. intros. auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset