let T be non empty TopSpace; :: thesis: 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
set rn = 0 ;
let pmet be Function of [:the carrier of T,the carrier of T:],REAL ; :: thesis: ( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) implies 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 )
assume that
A1: pmet is_a_pseudometric_of the carrier of T and
A2: for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ; :: thesis: 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
let A be non empty Subset of T; :: thesis: for p being Point of T st p in Cl A holds
(lower_bound pmet,A) . p = 0
let p be Point of T; :: thesis: ( p in Cl A implies (lower_bound pmet,A) . p = 0 )
A3: dom (lower_bound pmet,A) = the carrier of T by FUNCT_2:def 1;
reconsider Z = {0 }, infA = (lower_bound pmet,A) .: A as Subset of R^1 by TOPMETR:24;
infA c= Z

proof

let infa be set ; :: according to TARSKI:def 3 :: thesis: ( not infa in infA or infa in Z )
assume infa in infA ; :: thesis: infa in Z
then ex a being set st
( a in dom (lower_bound pmet,A) & a in A & infa = (lower_bound pmet,A) . a ) by FUNCT_1:def 12;
then infa = 0 by A1, Th6;
hence infa in Z by TARSKI:def 1; :: thesis: verum

end;

then A4: Cl infA c= Cl Z by PRE_TOPC:49;
reconsider InfA = lower_bound pmet,A as Function of T,R^1 by TOPMETR:24;
for p being Point of T holds dist pmet,p is continuous by A2, Th4;
then lower_bound pmet,A is continuous by A1, Th8;
then InfA is continuous by TOPREAL6:83;
then A5: InfA .: (Cl A) c= Cl (InfA .: A) by TOPS_2:57;
assume p in Cl A ; :: thesis: (lower_bound pmet,A) . p = 0
then A6: (lower_bound pmet,A) . p in (lower_bound pmet,A) .: (Cl A) by A3, FUNCT_1:def 12;
Z is closed by PCOMPS_1:10, TOPMETR:24;
then Z = Cl Z by PRE_TOPC:52;
then InfA .: (Cl A) c= Z by A4, A5, XBOOLE_1:1;
hence (lower_bound pmet,A) . p = 0 by A6, TARSKI:def 1; :: thesis: verum