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