let T be non empty TopSpace; :: thesis:
let pmet be Function of [: the carrier of T, the carrier of T:],REAL; :: thesis:
assume that
A1: pmet is_metric_of the carrier of T and
A2: for A being non empty Subset of T holds Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ; :: thesis:
set PM = SpaceMetr ( the carrier of T,pmet);
reconsider PM = SpaceMetr ( the carrier of T,pmet) as non empty MetrSpace by A1, PCOMPS_1:36;
A3: for x, y being Element of PM holds pmet . (x,y) = dist (x,y)

proof

let x, y be Element of PM; :: thesis:
PM = MetrStruct(# the carrier of T,pmet #) by A1, PCOMPS_1:def 7;
hence pmet . (x,y) = dist (x,y) by METRIC_1:def 1; :: thesis:

end;

A4: Family_open_set PM c= the topology of T

proof

let A be object ; :: according to TARSKI:def 3 :: thesis:
assume A5: A in Family_open_set PM ; :: thesis:
then reconsider AT = A as Subset of T by A1, PCOMPS_2:4;

per cases ;

suppose AT ` is empty ; :: thesis:

then AT ` = ([#] T) ` by XBOOLE_1:37;
then AT = the carrier of T by TOPS_1:1;
hence A in the topology of T by PRE_TOPC:def 1; :: thesis:

end;

suppose A6: not AT ` is empty ; :: thesis:

for x being set holds
( x in AT iff ex U being Subset of T st
( U is open & U c= AT & x in U ) )

proof

let x be set ; :: thesis:
( x in AT implies ex U being Subset of T st
( U is open & U c= AT & x in U ) )

proof

assume A7: x in AT ; :: thesis:
then reconsider xP = x as Element of PM by A1, PCOMPS_2:4;
consider r being Real such that
A8: r > 0 and
A9: Ball (xP,r) c= AT by A5, A7, PCOMPS_1:def 4;
reconsider xT = x as Element of T by A7;
A10: ex y being object st y in AT ` by A6;
reconsider B = Ball (xP,r) as Subset of T by A1, PCOMPS_2:4;
set Inf = { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } ;
AT ` c= B ` by A9, SUBSET_1:12;
then consider b being set such that
A11: b in B ` by A10;
B ` = { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 }

proof

thus B ` c= { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } :: according to XBOOLE_0:def 10 :: thesis:

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A12: y in B ` ; :: thesis:
(lower_bound (pmet,(B `))) . y = 0 by A1, A12, Th6, Th9;
hence y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } by A12; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } ; :: thesis:
then consider yT being Point of T such that
A13: y = yT and
A14: (lower_bound (pmet,(B `))) . yT = 0 ;
assume not y in B ` ; :: thesis:
then A15: yT in B by A13, XBOOLE_0:def 5;
reconsider yP = yT as Point of PM by A1, PCOMPS_2:4;
pmet is_a_pseudometric_of the carrier of T by A1, Th9;
then A16: ( not (dist (pmet,yT)) .: (B `) is empty & (dist (pmet,yT)) .: (B `) is bounded_below ) by A11, Lm1;
Ball (xP,r) in Family_open_set PM by PCOMPS_1:29;
then consider s being Real such that
A17: s > 0 and
A18: Ball (yP,s) c= Ball (xP,r) by A15, PCOMPS_1:def 4;
lower_bound ((dist (pmet,yT)) .: (B `)) = 0 by A14, Def3;
then consider rn being Real such that
A19: rn in (dist (pmet,yT)) .: (B `) and
A20: rn < 0 + s by A17, A16, SEQ_4:def 2;
consider z being object such that
A21: z in dom (dist (pmet,yT)) and
A22: z in B ` and
A23: rn = (dist (pmet,yT)) . z by A19, FUNCT_1:def 6;
reconsider zT = z as Point of T by A21;
reconsider zP = z as Point of PM by A1, A21, PCOMPS_2:4;
pmet . (yT,zT) < s by A20, A23, Def2;
then dist (yP,zP) < s by A3;
then zP in Ball (yP,s) by METRIC_1:11;
then B ` meets B by A18, A22, XBOOLE_0:3;
hence contradiction by XBOOLE_1:79; :: thesis:

end;

then B ` = Cl (B `) by A2, A11;
then A24: B is open by TOPS_1:4;
pmet . (xT,xT) = 0 by A1, PCOMPS_1:def 6;
then dist (xP,xP) < r by A3, A8;
then xP in B by METRIC_1:11;
hence ex U being Subset of T st
( U is open & U c= AT & x in U ) by A9, A24; :: thesis:

end;

hence ( x in AT iff ex U being Subset of T st
( U is open & U c= AT & x in U ) ) ; :: thesis:

end;

then AT is open by TOPS_1:25;
hence A in the topology of T by PRE_TOPC:def 2; :: thesis:

end;

the topology of T c= Family_open_set PM

proof

let A be object ; :: according to TARSKI:def 3 :: thesis:
assume A25: A in the topology of T ; :: thesis:
then reconsider AT = A as Subset of T ;
reconsider AP = A as Subset of PM by A1, A25, PCOMPS_2:4;

per cases ;

suppose AT ` is empty ; :: thesis:

then AT ` = ([#] T) ` by XBOOLE_1:37;
then AT = the carrier of T by TOPS_1:1;
then AT = the carrier of PM by A1, PCOMPS_2:4;
hence A in Family_open_set PM by PCOMPS_1:30; :: thesis:

end;

suppose A26: not AT ` is empty ; :: thesis:

for xP being Element of PM st xP in AP holds
ex r being Real st
( r > 0 & Ball (xP,r) c= AP )

proof

let xP be Element of PM; :: thesis:
assume A27: xP in AP ; :: thesis:
reconsider xT = xP as Element of T by A1, PCOMPS_2:4;
take r = (lower_bound (pmet,(AT `))) . xT; :: thesis:
A28: Ball (xP,r) c= AP

proof

pmet is_a_pseudometric_of the carrier of T by A1, Th9;
then A29: ( not (dist (pmet,xT)) .: (AT `) is empty & (dist (pmet,xT)) .: (AT `) is bounded_below ) by A26, Lm1;
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume that
A30: y in Ball (xP,r) and
A31: not y in AP ; :: thesis:
reconsider yP = y as Point of PM by A30;
A32: dist (xP,yP) < r by A30, METRIC_1:11;
reconsider yT = yP as Point of T by A1, PCOMPS_2:4;
A33: dom (dist (pmet,xT)) = the carrier of T by FUNCT_2:def 1;
yT in AT ` by A31, XBOOLE_0:def 5;
then (dist (pmet,xT)) . yT in (dist (pmet,xT)) .: (AT `) by A33, FUNCT_1:def 6;
then A34: lower_bound ((dist (pmet,xT)) .: (AT `)) <= (dist (pmet,xT)) . yT by A29, SEQ_4:def 2;
( (dist (pmet,xT)) . yT = pmet . (xT,yT) & lower_bound ((dist (pmet,xT)) .: (AT `)) = (lower_bound (pmet,(AT `))) . xT ) by Def2, Def3;
hence contradiction by A3, A32, A34; :: thesis:

end;

AT is open by A25, PRE_TOPC:def 2;
then AT ` = Cl (AT `) by PRE_TOPC:22;
then A35: AT ` = { p where p is Point of T : (lower_bound (pmet,(AT `))) . p = 0 } by A2, A26;
(lower_bound (pmet,(AT `))) . xT > 0

proof

assume (lower_bound (pmet,(AT `))) . xT <= 0 ; :: thesis:
then (lower_bound (pmet,(AT `))) . xT = 0 by A1, A26, Th5, Th9;
then xT in AT ` by A35;
then AT ` meets AT by A27, XBOOLE_0:3;
hence contradiction by XBOOLE_1:79; :: thesis:

end;

hence ( r > 0 & Ball (xP,r) c= AP ) by A28; :: thesis:

end;

hence A in Family_open_set PM by PCOMPS_1:def 4; :: thesis:

end;

then the topology of T = Family_open_set PM by A4;
hence T is metrizable by A1, PCOMPS_1:def 8; :: thesis: