proposition: Lemma MStotally_bounded_imp_located : forall (X : CPsMetricSpace) (P : X -> CProp), MStotally_bounded (SubPsMetricSpace P) -> located P.
proof: Proof. intros X P H. unfold located in |- *. intros x y. set (H0 := infimum_exists (SubPsMetricSpace P) (dsub'_as_cs_fun P x)) in *. set (H1 := H0 (dsub'_uni_continuous'' X P x) H y) in *. elim H1. intros x0 H2. elim H2. intros. simpl in |- *. exists x0. unfold set_glb_IR in |- *. split. intro x1. intro H6. apply a. generalize b. intros. elim H6. intros. exists x2. simpl in |- *. exact p. intros e H3. set (H7 := b e H3) in *. apply H7. Qed.
imports: CoRN.metrics.Prod_Sub