let M be non empty MetrSpace; :: thesis: for A, B being non empty Subset of (TopSpaceMetr M) holds { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } is open Subset of (TopSpaceMetr M)
set TM = TopSpaceMetr M;
let A, B be non empty Subset of (TopSpaceMetr M); :: thesis: { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } is open Subset of (TopSpaceMetr M)
set dA = dist_min A;
set dB = dist_min B;
consider g being Function of the carrier of (TopSpaceMetr M),the carrier of R^1 such that
A1: for p being Point of (TopSpaceMetr M)
for r1, r2 being real number st (dist_min A) . p = r1 & (dist_min B) . p = r2 holds
g . p = r1 - r2 and
A2: g is continuous by JGRAPH_2:31;
reconsider A = ].-infty ,0 .[ as Subset of R^1 by TOPMETR:24;
set gA = { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } ;
A3: ( [#] R^1 = {} implies [#] (TopSpaceMetr M) = {} ) ;
A4: g " A c= { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in g " A or x in { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } )
assume A5: x in g " A ; :: thesis: x in { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 }
then reconsider p = x as Point of (TopSpaceMetr M) ;
A6: ((dist_min A) . p) - ((dist_min B) . p) = g . x by A1;
g . x in A by A5, FUNCT_1:def 13;
then ((dist_min A) . p) - ((dist_min B) . p) < 0 by A6, XXREAL_1:233;
hence x in { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } ; :: thesis: verum

end;

A7: { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } c= g " A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } or x in g " A )
assume x in { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } ; :: thesis: x in g " A
then consider p being Point of (TopSpaceMetr M) such that
A8: p = x and
A9: ((dist_min A) . p) - ((dist_min B) . p) < 0 ;
g . p = ((dist_min A) . p) - ((dist_min B) . p) by A1;
then ( dom g = [#] (TopSpaceMetr M) & g . p in A ) by A9, FUNCT_2:def 1, XXREAL_1:233;
hence x in g " A by A8, FUNCT_1:def 13; :: thesis: verum

end;

A is open by BORSUK_5:63;
then g " A is open by A2, A3, TOPS_2:55;
hence { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } is open Subset of (TopSpaceMetr M) by A4, A7, XBOOLE_0:def 10; :: thesis: verum