proposition: Theorem Couple_as_union : forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y.
proof: Proof. intros x y; apply Extensionality_Ensembles; split; red. - intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets). - intros x0 H'; elim H'; auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset