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 & Family_open_set (SpaceMetr the carrier of T,metr) = the topology of T ) by PCOMPS_1:def 9;
set PM = SpaceMetr the carrier of T,metr;
reconsider PM = SpaceMetr the carrier of T,metr as non empty MetrSpace by PCOMPS_1:40, A1;
set TPM = TopSpaceMetr PM;
A4: 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 A5: ( D <> {} & D is closed & 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 )
reconsider p = p as Element of PM by A1, PCOMPS_2:8;
A6: ( D misses D ` & D <> {} & D is closed & p in D ` ) by A5, XBOOLE_1:79;
([#] T) \ D is open by A5;
then A7: ([#] T) \ D in the topology of T by PRE_TOPC:def 5;
reconsider D = D as Subset of (TopSpaceMetr PM) by A1, PCOMPS_2:8;
([#] (TopSpaceMetr PM)) \ D in Family_open_set PM by A1, A7, PCOMPS_2:8;
then ([#] (TopSpaceMetr PM)) \ D is open by PRE_TOPC:def 5;
then A8: ( ([#] (TopSpaceMetr PM)) \ D is open & D <> {} & D is closed & not p in D ) by A6, PRE_TOPC:def 6, XBOOLE_0:3;
ex r1 being Real st
( r1 > 0 & Ball p,r1 misses D )

proof

assume A9: for r1 being Real st r1 > 0 holds
Ball p,r1 meets D ; :: thesis: contradiction

now

let A be Subset of (TopSpaceMetr PM); :: thesis: ( A is open & p in A implies A meets D )
assume A10: ( A is open & p in A ) ; :: thesis: A meets D
then A in Family_open_set PM by PRE_TOPC:def 5;
then consider r2 being Real such that
A11: ( r2 > 0 & Ball p,r2 c= A ) by A10, PCOMPS_1:def 5;
Ball p,r2 meets D by A9, A11;
then consider x being set such that
A12: ( x in Ball p,r2 & x in D ) by XBOOLE_0:3;
thus A meets D by A11, A12, XBOOLE_0:3; :: thesis: verum

end;

then p in Cl D by PRE_TOPC:def 13;
hence contradiction by A8, PRE_TOPC:52; :: thesis: verum

end;

then consider r1 being Real such that
A13: ( r1 > 0 & Ball p,r1 misses D ) ;
set r2 = r1 / 2;
set r4 = (r1 / 2) / 2;
r1 / 2 > 0 by A13, XREAL_1:141;
then ( r1 / 2 > 0 & (r1 / 2) / 2 > 0 ) by XREAL_1:141;
then A14: ( 0 < (r1 / 2) / 2 & (r1 / 2) / 2 < ((r1 / 2) / 2) + ((r1 / 2) / 2) & r1 / 2 < (r1 / 2) + (r1 / 2) & dist p,p < (r1 / 2) / 2 ) by METRIC_1:1, XREAL_1:31;
A15: 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 set such that
A16: ( x in D & not x in ([#] PM) \ (cl_Ball p,(r1 / 2)) ) by TARSKI:def 3;
reconsider x = x as Element of PM by A16;
( x in D & x in cl_Ball p,(r1 / 2) ) by A16, XBOOLE_0:def 5;
then dist p,x <= r1 / 2 by METRIC_1:13;
then dist p,x < r1 by A14, XXREAL_0:2;
then x in Ball p,r1 by METRIC_1:12;
hence contradiction by A13, A16, XBOOLE_0:3; :: thesis: verum

end;

A17: 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 set such that
A18: ( x in Ball p,((r1 / 2) / 2) & x in ([#] PM) \ (cl_Ball p,(r1 / 2)) ) by XBOOLE_0:3;
reconsider x = x as Element of PM by A18;
( x in Ball p,((r1 / 2) / 2) & not x in cl_Ball p,(r1 / 2) ) by A18, XBOOLE_0:def 5;
then ( dist p,x < (r1 / 2) / 2 & dist p,x > r1 / 2 ) by METRIC_1:12, METRIC_1:13;
hence contradiction by A14, XXREAL_0:2; :: thesis: verum

end;

set B = ([#] PM) \ (cl_Ball p,(r1 / 2));
set A = Ball p,((r1 / 2) / 2);
A19: ( ([#] 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:33;
then reconsider A = Ball p,((r1 / 2) / 2), B = ([#] PM) \ (cl_Ball p,(r1 / 2)) as Subset of T by A1;
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 )
thus ( A is open & B is open & p in A & D c= B & A misses B ) by A1, A14, A15, A17, A19, METRIC_1:12, PRE_TOPC:def 5; :: 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 A20: 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:8;
( TopSpaceMetr PM is T_2 & p is Element of (TopSpaceMetr PM) & q is Element of (TopSpaceMetr PM) & not p = q ) by A20, PCOMPS_1:38;
then consider A, B being Subset of (TopSpaceMetr PM) such that
A21: ( A is open & B is open & p in A & q in B & A misses B ) by PRE_TOPC:def 16;
reconsider A = A, B = B as Subset of T by A1, PCOMPS_2:8;
( A in the topology of T & B in the topology of T ) by A1, A21, PRE_TOPC:def 5;
then ( A is Subset of T & B is Subset of T & A is open & B is open & p in A & not q in A & q in B & not p in B ) by A21, PRE_TOPC:def 5, 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 ) ; :: thesis: verum

end;

hence ( T is regular & T is T_1 ) by A4, COMPTS_1:def 5, URYSOHN1:def 9; :: thesis: verum