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 )

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 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

for p, q being Point of T st not p = q holds
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 )

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)))

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)))

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;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

then consider r1 being Real such that
assume A10:
for r1 being Real st r1 > 0 holds

Ball (p,r1) meets D ; :: thesis: contradiction

hence contradiction by A8, A9, PRE_TOPC:22; :: thesis: verum

end;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

then
p in Cl D
by PRE_TOPC:def 7;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;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

hence contradiction by A8, A9, PRE_TOPC:22; :: thesis: verum

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

set r4 = (r1 / 2) / 2;
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;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

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

set A = Ball (p,((r1 / 2) / 2));
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;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

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

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

hence
( T is regular & T is T_1 )
by A3, URYSOHN1:def 7; :: thesis: verum
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;( 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