let T be non empty TopSpace; :: thesis: for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_metric_of the carrier of T & ( for A being non empty Subset of T holds Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ) holds
T is metrizable

let pmet be Function of [: the carrier of T, the carrier of T:],REAL; :: thesis: ( pmet is_metric_of the carrier of T & ( for A being non empty Subset of T holds Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ) implies T is metrizable )
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: T is metrizable
set PM = SpaceMetr ( the carrier of T,pmet);
reconsider PM = SpaceMetr ( the carrier of T,pmet) as non empty MetrSpace by ;
A3: for x, y being Element of PM holds pmet . (x,y) = dist (x,y)
proof
let x, y be Element of PM; :: thesis: pmet . (x,y) = dist (x,y)
PM = MetrStruct(# the carrier of T,pmet #) by ;
hence pmet . (x,y) = dist (x,y) by METRIC_1:def 1; :: thesis: verum
end;
A4: Family_open_set PM c= the topology of T
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in Family_open_set PM or A in the topology of T )
assume A5: A in Family_open_set PM ; :: thesis: A in the topology of T
then reconsider AT = A as Subset of T by ;
per cases ( AT ` is empty or not AT ` is empty ) ;
suppose A6: not AT ` is empty ; :: thesis: A in the topology of T
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 iff ex U being Subset of T st
( U is open & U c= AT & x in U ) )

( 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: ex U being Subset of T st
( U is open & U c= AT & x in U )

then reconsider xP = x as Element of PM by ;
consider r being Real such that
A8: r > 0 and
A9: Ball (xP,r) c= AT by ;
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 ;
set Inf = { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } ;
AT ` c= B ` by ;
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: { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } c= B `
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in B ` or y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } )
assume A12: y in B ` ; :: thesis: y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 }
(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: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } or y in B ` )
assume y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } ; :: thesis: y in B `
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: contradiction
then A15: yT in B by ;
reconsider yP = yT as Point of PM by ;
pmet is_a_pseudometric_of the carrier of T by ;
then A16: ( not (dist (pmet,yT)) .: (B `) is empty & (dist (pmet,yT)) .: (B `) is bounded_below ) by ;
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 ;
lower_bound ((dist (pmet,yT)) .: (B `)) = 0 by ;
then consider rn being Real such that
A19: rn in (dist (pmet,yT)) .: (B `) and
A20: rn < 0 + s by ;
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 ;
reconsider zT = z as Point of T by A21;
reconsider zP = z as Point of PM by ;
pmet . (yT,zT) < s by ;
then dist (yP,zP) < s by A3;
then zP in Ball (yP,s) by METRIC_1:11;
then B ` meets B by ;
hence contradiction by XBOOLE_1:79; :: thesis: verum
end;
then B ` = Cl (B `) by ;
then A24: B is open by TOPS_1:4;
pmet . (xT,xT) = 0 by ;
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 ; :: thesis: verum
end;
hence ( x in AT iff ex U being Subset of T st
( U is open & U c= AT & x in U ) ) ; :: thesis: verum
end;
then AT is open by TOPS_1:25;
hence A in the topology of T by PRE_TOPC:def 2; :: thesis: verum
end;
end;
end;
the topology of T c= Family_open_set PM
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in the topology of T or A in Family_open_set PM )
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 ;
per cases ( AT ` is empty or not AT ` is empty ) ;
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: ( xP in AP implies ex r being Real st
( r > 0 & Ball (xP,r) c= AP ) )

assume A27: xP in AP ; :: thesis: ex r being Real st
( r > 0 & Ball (xP,r) c= AP )

reconsider xT = xP as Element of T by ;
take r = (lower_bound (pmet,(AT `))) . xT; :: thesis: ( r > 0 & Ball (xP,r) c= AP )
A28: Ball (xP,r) c= AP
proof
pmet is_a_pseudometric_of the carrier of T by ;
then A29: ( not (dist (pmet,xT)) .: (AT `) is empty & (dist (pmet,xT)) .: (AT `) is bounded_below ) by ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball (xP,r) or y in AP )
assume that
A30: y in Ball (xP,r) and
A31: not y in AP ; :: thesis: contradiction
reconsider yP = y as Point of PM by A30;
A32: dist (xP,yP) < r by ;
reconsider yT = yP as Point of T by ;
A33: dom (dist (pmet,xT)) = the carrier of T by FUNCT_2:def 1;
yT in AT ` by ;
then (dist (pmet,xT)) . yT in (dist (pmet,xT)) .: (AT `) by ;
then A34: lower_bound ((dist (pmet,xT)) .: (AT `)) <= (dist (pmet,xT)) . yT by ;
( (dist (pmet,xT)) . yT = pmet . (xT,yT) & lower_bound ((dist (pmet,xT)) .: (AT `)) = (lower_bound (pmet,(AT `))) . xT ) by ;
hence contradiction by A3, A32, A34; :: thesis: verum
end;
AT is open by ;
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 ;
(lower_bound (pmet,(AT `))) . xT > 0
proof
assume (lower_bound (pmet,(AT `))) . xT <= 0 ; :: thesis: contradiction
then (lower_bound (pmet,(AT `))) . xT = 0 by A1, A26, Th5, Th9;
then xT in AT ` by A35;
then AT ` meets AT by ;
hence contradiction by XBOOLE_1:79; :: thesis: verum
end;
hence ( r > 0 & Ball (xP,r) c= AP ) by A28; :: thesis: verum
end;
hence A in Family_open_set PM by PCOMPS_1:def 4; :: thesis: verum
end;
end;
end;
then the topology of T = Family_open_set PM by A4;
hence T is metrizable by ; :: thesis: verum