let TM be metrizable TopSpace; :: thesis: for A, B being Subset of TM st A,B are_separated holds
ex U, W being open Subset of TM st
( A c= U & B c= W & U misses W )
let A, B be Subset of TM; :: thesis: ( A,B are_separated implies ex U, W being open Subset of TM st
( A c= U & B c= W & U misses W ) )
assume A1: A,B are_separated ; :: thesis: ex U, W being open Subset of TM st
( A c= U & B c= W & U misses W )
set TOP = the topology of TM;
set cTM = the carrier of TM;
consider metr being Function of [:the carrier of TM,the carrier of TM:],REAL such that
A2: metr is_metric_of the carrier of TM and
A3: Family_open_set (SpaceMetr the carrier of TM,metr) = the topology of TM by PCOMPS_1:def 9;

per cases ( A = {} TM or B = {} TM or ( A <> {} TM & B <> {} TM ) ) ;

suppose A4: A = {} TM ; :: thesis: ex U, W being open Subset of TM st
( A c= U & B c= W & U misses W )

take U = {} TM; :: thesis: ex W being open Subset of TM st
( A c= U & B c= W & U misses W )
take W = [#] TM; :: thesis: ( A c= U & B c= W & U misses W )
thus ( A c= U & B c= W & U misses W ) by A4, XBOOLE_1:65; :: thesis: verum

end;

suppose A5: B = {} TM ; :: thesis: ex U, W being open Subset of TM st
( A c= U & B c= W & U misses W )

take U = [#] TM; :: thesis: ex W being open Subset of TM st
( A c= U & B c= W & U misses W )
take W = {} TM; :: thesis: ( A c= U & B c= W & U misses W )
thus ( A c= U & B c= W & U misses W ) by A5, XBOOLE_1:65; :: thesis: verum

end;

suppose A6: ( A <> {} TM & B <> {} TM ) ; :: thesis: ex U, W being open Subset of TM st
( A c= U & B c= W & U misses W )

then A7: not TM is empty ;
then reconsider Tm = SpaceMetr the carrier of TM,metr as non empty MetrSpace by A2, PCOMPS_1:40;
set TTm = TopSpaceMetr Tm;
reconsider A' = A, B' = B as Subset of (TopSpaceMetr Tm) by A2, A7, PCOMPS_2:8;
set dA = dist_min A';
set dB = dist_min B';
reconsider U = { p where p is Point of Tm : ((dist_min A') . p) - ((dist_min B') . p) < 0 } , W = { p where p is Point of Tm : ((dist_min B') . p) - ((dist_min A') . p) < 0 } as open Subset of (TopSpaceMetr Tm) by A6, Lm11;
( U in Family_open_set Tm & W in Family_open_set Tm ) by PRE_TOPC:def 5;
then reconsider U = U, W = W as open Subset of TM by A3, PRE_TOPC:def 5;
take U ; :: thesis: ex W being open Subset of TM st
( A c= U & B c= W & U misses W )
take W ; :: thesis: ( A c= U & B c= W & U misses W )
A8: [#] TM = [#] (TopSpaceMetr Tm) by A2, A7, PCOMPS_2:8;
thus A c= U :: thesis: ( B c= W & U misses W )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in U )
assume A9: x in A ; :: thesis: x in U
then reconsider p = x as Point of Tm by A2, A7, PCOMPS_2:8;
A10: (dist_min A') . p = 0 by A9, HAUSDORF:5;
A misses Cl B by A1, CONNSP_1:def 1;
then not x in Cl B by A9, XBOOLE_0:3;
then not x in Cl B' by A3, A8, TOPS_3:80;
then A11: (dist_min B') . p <> 0 by A6, HAUSDORF:10;
(dist_min B') . p >= 0 by A6, JORDAN1K:9;
then ((dist_min A') . p) - ((dist_min B') . p) < 0 by A11, A10;
hence x in U ; :: thesis: verum

end;

thus B c= W :: thesis: U misses W

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in W )
assume A12: x in B ; :: thesis: x in W
then reconsider p = x as Point of Tm by A2, A7, PCOMPS_2:8;
A13: (dist_min B') . p = 0 by A12, HAUSDORF:5;
B misses Cl A by A1, CONNSP_1:def 1;
then not x in Cl A by A12, XBOOLE_0:3;
then not x in Cl A' by A3, A8, TOPS_3:80;
then A14: (dist_min A') . p <> 0 by A6, HAUSDORF:10;
(dist_min A') . p >= 0 by A6, JORDAN1K:9;
then ((dist_min B') . p) - ((dist_min A') . p) < 0 by A14, A13;
hence x in W ; :: thesis: verum

end;

thus U misses W :: thesis: verum

proof

assume U meets W ; :: thesis: contradiction
then consider x being set such that
A15: x in U and
A16: x in W by XBOOLE_0:3;
consider p being Point of Tm such that
A17: p = x and
A18: ((dist_min B') . p) - ((dist_min A') . p) < 0 by A16;
ex q being Point of Tm st
( q = x & ((dist_min A') . q) - ((dist_min B') . q) < 0 ) by A15;
then - (((dist_min A') . p) - ((dist_min B') . p)) > - 0 by A17;
hence contradiction by A18; :: thesis: verum

end;

end;

end;