proposition: Theorem Intersection_commutative : forall A B:Ensemble U, Intersection U A B = Intersection U B A.
proof: Proof. intros A B. apply Extensionality_Ensembles. split; red; intros x H'; elim H'; auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset