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 A1, PCOMPS_1:36;
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 A4, A5, PRE_TOPC:def 2;
reconsider p = p as Element of PM by A1, PCOMPS_2:4;
A7: D misses D ` by XBOOLE_1:79;
reconsider D = D as Subset of (TopSpaceMetr PM) by A1, PCOMPS_2:4;
([#] (TopSpaceMetr PM)) \ D in Family_open_set PM by A1, A2, A6, PCOMPS_2:4;
then ([#] (TopSpaceMetr PM)) \ D is open by PRE_TOPC:def 2;
then A8: D is closed by PRE_TOPC:def 3;
A9: not p in D by A5, A7, XBOOLE_0:3;
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 (TopSpaceMetr PM) st A is open & p in A holds
A meets D

let A be Subset of (TopSpaceMetr PM); :: 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 A11, PRE_TOPC:def 2;
then consider r2 being Real such that
A13: r2 > 0 and
A14: Ball (p,r2) c= A by A12, PCOMPS_1:def 4;
Ball (p,r2) meets D by A10, A13;
then ex x being object st
( x in Ball (p,r2) & x in D ) by XBOOLE_0:3;
hence A meets D by A14, XBOOLE_0:3; :: 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 A15, XREAL_1:29;
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 A20, XBOOLE_0:def 5;
then dist (p,x) <= r1 / 2 by METRIC_1:12;
then dist (p,x) < r1 by A17, XXREAL_0:2;
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 A15, XREAL_1:139;
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 A25, XBOOLE_0:def 5;
then A26: dist (p,x) > r1 / 2 by METRIC_1:12;
dist (p,x) < (r1 / 2) / 2 by A24, METRIC_1:11;
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 Th14, PCOMPS_1:29;
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 A21, XREAL_1:139;
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 A2, A18, A23, A27, METRIC_1:11, PRE_TOPC:def 2; :: 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 (TopSpaceMetr PM) by A1, PCOMPS_2:4;
TopSpaceMetr PM is T_2 by PCOMPS_1:34;
then consider A, B being Subset of (TopSpaceMetr PM) 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 A28, PRE_TOPC:def 10;
reconsider A = A, B = B as Subset of T by A1, PCOMPS_2:4;
A in the topology of T by A2, A29, PRE_TOPC:def 2;
then A33: A is open by PRE_TOPC:def 2;
B in the topology of T by A2, A30, PRE_TOPC:def 2;
then A34: B is open by PRE_TOPC:def 2;
( not q in A & not p in B ) by A31, A32, XBOOLE_0:3;
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 A31, A33, A34; :: thesis: verum

end;

hence ( T is regular & T is T_1 ) by A3, URYSOHN1:def 7; :: thesis: verum