proposition: Theorem Intersection_is_Glb : forall A a b:Ensemble U, Included U a A -> Included U b A -> Glb (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Intersection U a b).
proof: Proof. intros A a b H' H'0. apply Glb_definition; simpl. - apply Lower_Bound_definition; simpl; auto with sets. + apply Definition_of_Power_set. generalize Inclusion_is_transitive; intro IT; red in IT; apply IT with a; auto with sets. + intros y H'1; elim H'1; auto with sets. - intros y H'1; elim H'1; simpl; auto with sets. Qed.
imports: Ensembles Relations_1 Relations_1_facts Partial_Order Cpo