proposition: Theorem Intersection_decreases_l : forall a b:Ensemble U, Included U (Intersection U a b) a.
proof: Proof. intros a b; red. intros x H'; elim H'; auto with sets. Qed.
imports: Ensembles Relations_1 Relations_1_facts Partial_Order Cpo