proposition: Theorem Intersection_maximal : forall a b X:Ensemble U, Included U X a -> Included U X b -> Included U X (Intersection U a b).
proof: Proof. auto with sets. Qed.
imports: Ensembles Relations_1 Relations_1_facts Partial_Order Cpo