let T be non empty TopSpace; :: thesis: ( T is metrizable implies ( T is regular & T is T_1 ) )
assume T is metrizable ; :: thesis: ( T is regular & T is T_1 )
then consider metr being Function of [: the carrier of T, the carrier of T:],REAL such that
A1: metr is_metric_of the carrier of T and
A2: Family_open_set (SpaceMetr ( the carrier of T,metr)) = the topology of T ;
set PM = SpaceMetr ( the carrier of T,metr);
reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by ;
set TPM = TopSpaceMetr PM;
A3: for p being Element of T
for D being Subset of T st D <> {} & D is closed & p in D ` holds
ex A, B being Subset of T st
( A is open & B is open & p in A & D c= B & A misses B )
proof
let p be Element of T; :: thesis: for D being Subset of T st D <> {} & D is closed & p in D ` holds
ex A, B being Subset of T st
( A is open & B is open & p in A & D c= B & A misses B )

let D be Subset of T; :: thesis: ( D <> {} & D is closed & p in D ` implies ex A, B being Subset of T st
( A is open & B is open & p in A & D c= B & A misses B ) )

assume that
D <> {} and
A4: D is closed and
A5: p in D ` ; :: thesis: ex A, B being Subset of T st
( A is open & B is open & p in A & D c= B & A misses B )

A6: ([#] T) \ D in the topology of T by ;
reconsider p = p as Element of PM by ;
A7: D misses D ` by XBOOLE_1:79;
reconsider D = D as Subset of () by ;
([#] ()) \ D in Family_open_set PM by ;
then ([#] ()) \ D is open by PRE_TOPC:def 2;
then A8: D is closed by PRE_TOPC:def 3;
A9: not p in D by ;
ex r1 being Real st
( r1 > 0 & Ball (p,r1) misses D )
proof
assume A10: for r1 being Real st r1 > 0 holds
Ball (p,r1) meets D ; :: thesis: contradiction
now :: thesis: for A being Subset of () st A is open & p in A holds
A meets D
let A be Subset of (); :: thesis: ( A is open & p in A implies A meets D )
assume that
A11: A is open and
A12: p in A ; :: thesis: A meets D
A in Family_open_set PM by ;
then consider r2 being Real such that
A13: r2 > 0 and
A14: Ball (p,r2) c= A by ;
Ball (p,r2) meets D by ;
then ex x being object st
( x in Ball (p,r2) & x in D ) by XBOOLE_0:3;
hence A meets D by ; :: thesis: verum
end;
then p in Cl D by PRE_TOPC:def 7;
hence contradiction by A8, A9, PRE_TOPC:22; :: thesis: verum
end;
then consider r1 being Real such that
A15: r1 > 0 and
A16: Ball (p,r1) misses D ;
set r2 = r1 / 2;
A17: r1 / 2 < (r1 / 2) + (r1 / 2) by ;
A18: D c= ([#] PM) \ (cl_Ball (p,(r1 / 2)))
proof
assume not D c= ([#] PM) \ (cl_Ball (p,(r1 / 2))) ; :: thesis: contradiction
then consider x being object such that
A19: x in D and
A20: not x in ([#] PM) \ (cl_Ball (p,(r1 / 2))) ;
reconsider x = x as Element of PM by A19;
x in cl_Ball (p,(r1 / 2)) by ;
then dist (p,x) <= r1 / 2 by METRIC_1:12;
then dist (p,x) < r1 by ;
then x in Ball (p,r1) by METRIC_1:11;
hence contradiction by A16, A19, XBOOLE_0:3; :: thesis: verum
end;
set r4 = (r1 / 2) / 2;
A21: r1 / 2 > 0 by ;
then A22: (r1 / 2) / 2 < ((r1 / 2) / 2) + ((r1 / 2) / 2) by XREAL_1:29;
A23: Ball (p,((r1 / 2) / 2)) misses ([#] PM) \ (cl_Ball (p,(r1 / 2)))
proof
assume Ball (p,((r1 / 2) / 2)) meets ([#] PM) \ (cl_Ball (p,(r1 / 2))) ; :: thesis: contradiction
then consider x being object such that
A24: x in Ball (p,((r1 / 2) / 2)) and
A25: x in ([#] PM) \ (cl_Ball (p,(r1 / 2))) by XBOOLE_0:3;
reconsider x = x as Element of PM by A24;
not x in cl_Ball (p,(r1 / 2)) by ;
then A26: dist (p,x) > r1 / 2 by METRIC_1:12;
dist (p,x) < (r1 / 2) / 2 by ;
hence contradiction by A22, A26, XXREAL_0:2; :: thesis: verum
end;
set A = Ball (p,((r1 / 2) / 2));
set B = ([#] PM) \ (cl_Ball (p,(r1 / 2)));
A27: ( ([#] PM) \ (cl_Ball (p,(r1 / 2))) in Family_open_set PM & Ball (p,((r1 / 2) / 2)) in Family_open_set PM ) by ;
then reconsider A = Ball (p,((r1 / 2) / 2)), B = ([#] PM) \ (cl_Ball (p,(r1 / 2))) as Subset of T by A2;
take A ; :: thesis: ex B being Subset of T st
( A is open & B is open & p in A & D c= B & A misses B )

take B ; :: thesis: ( A is open & B is open & p in A & D c= B & A misses B )
(r1 / 2) / 2 > 0 by ;
then dist (p,p) < (r1 / 2) / 2 by METRIC_1:1;
hence ( A is open & B is open & p in A & D c= B & A misses B ) by ; :: thesis: verum
end;
for p, q being Point of T st not p = q holds
ex A, B being Subset of T st
( A is open & B is open & p in A & not q in A & q in B & not p in B )
proof
let p, q be Point of T; :: thesis: ( not p = q implies ex A, B being Subset of T st
( A is open & B is open & p in A & not q in A & q in B & not p in B ) )

assume A28: not p = q ; :: thesis: ex A, B being Subset of T st
( A is open & B is open & p in A & not q in A & q in B & not p in B )

reconsider p = p, q = q as Element of () by ;
TopSpaceMetr PM is T_2 by PCOMPS_1:34;
then consider A, B being Subset of () such that
A29: A is open and
A30: B is open and
A31: ( p in A & q in B ) and
A32: A misses B by ;
reconsider A = A, B = B as Subset of T by ;
A in the topology of T by ;
then A33: A is open by PRE_TOPC:def 2;
B in the topology of T by ;
then A34: B is open by PRE_TOPC:def 2;
( not q in A & not p in B ) by ;
hence ex A, B being Subset of T st
( A is open & B is open & p in A & not q in A & q in B & not p in B ) by ; :: thesis: verum
end;
hence ( T is regular & T is T_1 ) by ; :: thesis: verum