proposition: Lemma Distributivity_l : forall (A B C : Ensemble U), Intersection U (Union U A B) C = Union U (Intersection U A C) (Intersection U B C).
proof: Proof. intros A B C. rewrite Intersection_commutative. rewrite Distributivity. f_equal; apply Intersection_commutative. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset