let PM be non empty MetrSpace; :: thesis: TopSpaceMetr PM is T_2
set TPS = TopSpaceMetr PM;
for x, y being Element of (TopSpaceMetr PM) st not x = y holds
ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )

proof

let x, y be Element of (TopSpaceMetr PM); :: thesis: ( not x = y implies ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V ) )
assume A1: not x = y ; :: thesis: ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )
reconsider x = x, y = y as Element of PM ;
set r = (dist (x,y)) / 2;
dist (x,y) <> 0 by A1, METRIC_1:2;
then dist (x,y) > 0 by METRIC_1:5;
then A2: (dist (x,y)) / 2 > 0 by XREAL_1:139;
ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )

proof

set V = Ball (y,((dist (x,y)) / 2));
set W = Ball (x,((dist (x,y)) / 2));
A3: ( Ball (x,((dist (x,y)) / 2)) in Family_open_set PM & Ball (y,((dist (x,y)) / 2)) in Family_open_set PM ) by Th29;
reconsider W = Ball (x,((dist (x,y)) / 2)), V = Ball (y,((dist (x,y)) / 2)) as Subset of (TopSpaceMetr PM) ;
A4: for z being object holds not z in W /\ V

proof

let z be object ; :: thesis: not z in W /\ V
assume A5: z in W /\ V ; :: thesis: contradiction
then reconsider z = z as Element of PM ;
z in V by A5, XBOOLE_0:def 4;
then A6: dist (y,z) < (dist (x,y)) / 2 by METRIC_1:11;
z in W by A5, XBOOLE_0:def 4;
then dist (x,z) < (dist (x,y)) / 2 by METRIC_1:11;
then (dist (x,z)) + (dist (y,z)) < ((dist (x,y)) / 2) + ((dist (x,y)) / 2) by A6, XREAL_1:8;
hence contradiction by METRIC_1:4; :: thesis: verum

end;

take W ; :: thesis: ex V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )
take V ; :: thesis: ( W is open & V is open & x in W & y in V & W misses V )
( dist (x,x) = 0 & dist (y,y) = 0 ) by METRIC_1:1;
hence ( W is open & V is open & x in W & y in V & W misses V ) by A2, A3, A4, METRIC_1:11, PRE_TOPC:def 2, XBOOLE_0:4; :: thesis: verum

end;

hence ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V ) ; :: thesis: verum

end;

hence TopSpaceMetr PM is T_2 by PRE_TOPC:def 10; :: thesis: verum