let PM be non empty MetrSpace; :: thesis: TopSpaceMetr PM is Hausdorff
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:141;
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 Th33;
reconsider W = Ball x,((dist x,y) / 2), V = Ball y,((dist x,y) / 2) as Subset of (TopSpaceMetr PM) ;
A4: for z being set holds not z in W /\ V

proof

let z be set ; :: 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:12;
z in W by A5, XBOOLE_0:def 4;
then dist x,z < (dist x,y) / 2 by METRIC_1:12;
then (dist x,z) + (dist y,z) < ((dist x,y) / 2) + ((dist x,y) / 2) by A6, XREAL_1:10;
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:12, PRE_TOPC:def 5, 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 Hausdorff by PRE_TOPC:def 16; :: thesis: verum