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 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 A1, PCOMPS_1:40;
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 5;
reconsider p = p as Element of PM by A1, PCOMPS_2:8;
A7: D misses D ` by XBOOLE_1:79;
reconsider D = D as Subset of (TopSpaceMetr PM) by A1, PCOMPS_2:8;
([#] (TopSpaceMetr PM)) \ D in Family_open_set PM by A1, A2, A6, PCOMPS_2:8;
then ([#] (TopSpaceMetr PM)) \ D is open by PRE_TOPC:def 5;
then A8: D is closed by PRE_TOPC:def 6;
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

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 5;
then consider r2 being Real such that
A13: r2 > 0 and
A14: Ball p,r2 c= A by A12, PCOMPS_1:def 5;
Ball p,r2 meets D by A10, A13;
then ex x being set 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 13;
hence contradiction by A8, A9, PRE_TOPC:52; :: 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:31;
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 set such that
A19: x in D and
A20: not x in ([#] PM) \ (cl_Ball p,(r1 / 2)) by TARSKI:def 3;
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:13;
then dist p,x < r1 by A17, XXREAL_0:2;
then x in Ball p,r1 by METRIC_1:12;
hence contradiction by A16, A19, XBOOLE_0:3; :: thesis: verum

end;

set r4 = (r1 / 2) / 2;
A21: r1 / 2 > 0 by A15, XREAL_1:141;
then A22: (r1 / 2) / 2 < ((r1 / 2) / 2) + ((r1 / 2) / 2) by XREAL_1:31;
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 set 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:13;
dist p,x < (r1 / 2) / 2 by A24, METRIC_1:12;
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:33;
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:141;
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: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 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:8;
TopSpaceMetr PM is T_2 by PCOMPS_1:38;
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 16;
reconsider A = A, B = B as Subset of T by A1, PCOMPS_2:8;
A in the topology of T by A2, A29, PRE_TOPC:def 5;
then A33: A is open by PRE_TOPC:def 5;
B in the topology of T by A2, A30, PRE_TOPC:def 5;
then A34: B is open by PRE_TOPC:def 5;
( 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, COMPTS_1:def 5, URYSOHN1:def 9; :: thesis: verum