proposition: Theorem Triple_as_union : forall x y z:U, Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) = Triple U x y z.
proof: Proof. intros x y z; apply Extensionality_Ensembles; split; red. - intros x0 H'; elim H'. + intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets). + 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