for T being non empty TopSpace
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) holds
for A being non empty Subset of T
for p being Point of T st p in Cl A holds
(lower_bound (pmet,A)) . p = 0