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 st (dist_min A) . p = r1 & (dist_min B) . p = r2 holds
g . p = r1 - r2 and
A2: g is continuous by JGRAPH_2:21;
set gA = { p where p is Point of (TopSpaceMetr M) : ((dist_min A) . p) - ((dist_min B) . p) < 0 } ;
reconsider A = ].-infty,0.[ as Subset of R^1 by TOPMETR:17;
A3: A is open by BORSUK_5:40;
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 object ; :: 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: g . x in A by A5, FUNCT_1:def 7;
((dist_min A) . p) - ((dist_min B) . p) = g . x by A1;
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 object ; :: 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 7; :: thesis: verum

end;

( [#] R^1 = {} implies [#] (TopSpaceMetr M) = {} ) ;
then g " A is open by A2, A3, TOPS_2:43;
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