proposition: Theorem Union_minimal : forall a b X:Ensemble U, Included U a X -> Included U b X -> Included U (Union U a b) X.
proof: Proof. intros a b X H' H'0; red. intros x H'1; elim H'1; auto with sets. Qed.
imports: Ensembles Relations_1 Relations_1_facts Partial_Order Cpo