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 pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) holds
for A being non empty Subset of
for p being Point of st p in Cl A holds
(inf 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 pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) implies for A being non empty Subset of
for p being Point of st p in Cl A holds
(inf pmet,A) . p = 0 )
assume that
A1: pmet is_a_pseudometric_of the carrier of T and
A2: for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ; :: thesis: for A being non empty Subset of
for p being Point of st p in Cl A holds
(inf pmet,A) . p = 0
let A be non empty Subset of ; :: thesis: for p being Point of st p in Cl A holds
(inf pmet,A) . p = 0
let p be Point of ; :: thesis: ( p in Cl A implies (inf pmet,A) . p = 0 )
A3: dom (inf pmet,A) = the carrier of T by FUNCT_2:def 1;
reconsider Z = {0 }, infA = (inf pmet,A) .: A as Subset of 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 (inf pmet,A) & a in A & infa = (inf 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 = inf pmet,A as Function of T,R^1 by TOPMETR:24;
for p being Point of holds dist pmet,p is continuous by A2, Th4;
then inf 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: (inf pmet,A) . p = 0
then A6: (inf pmet,A) . p in (inf 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 (inf pmet,A) . p = 0 by A6, TARSKI:def 1; :: thesis: verum