proposition: Theorem Distributivity : forall A B C:Ensemble U, Intersection U A (Union U B C) = Union U (Intersection U A B) (Intersection U A C).
proof: Proof. intros A B C. apply Extensionality_Ensembles. split; red; intros x H'. - elim H'. intros x0 H'0 H'1; generalize H'0. elim H'1; auto with sets. - elim H'; intros x0 H'0; elim H'0; auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset