let M be non empty MetrSpace; :: thesis: for A being non empty Subset of (TopSpaceMetr M)
for r being Real holds { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } is open Subset of (TopSpaceMetr M)
set TM = TopSpaceMetr M;
let A be non empty Subset of (TopSpaceMetr M); :: thesis: for r being Real holds { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } is open Subset of (TopSpaceMetr M)
let r be Real; :: thesis: { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } is open Subset of (TopSpaceMetr M)
set d = dist_min A;
reconsider A = ].-infty,r.[ as Subset of R^1 by TOPMETR:17;
set dA = { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } ;
A1: { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } c= (dist_min A) " 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 < r } or x in (dist_min A) " A )
assume x in { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } ; :: thesis: x in (dist_min A) " A
then consider p being Point of (TopSpaceMetr M) such that
A2: p = x and
A3: (dist_min A) . p < r ;
( dom (dist_min A) = [#] (TopSpaceMetr M) & (dist_min A) . p in A ) by A3, FUNCT_2:def 1, XXREAL_1:233;
hence x in (dist_min A) " A by A2, FUNCT_1:def 7; :: thesis: verum

end;

A4: (dist_min A) " A c= { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (dist_min A) " A or x in { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } )
assume A5: x in (dist_min A) " A ; :: thesis: x in { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r }
then reconsider p = x as Point of (TopSpaceMetr M) ;
(dist_min A) . p in A by A5, FUNCT_1:def 7;
then (dist_min A) . p < r by XXREAL_1:233;
hence x in { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } ; :: thesis: verum

end;

A6: A is open by BORSUK_5:40;
( [#] R^1 = {} implies [#] (TopSpaceMetr M) = {} ) ;
then (dist_min A) " A is open by A6, TOPS_2:43;
hence { p where p is Point of (TopSpaceMetr M) : (dist_min A) . p < r } is open Subset of (TopSpaceMetr M) by A1, A4, XBOOLE_0:def 10; :: thesis: verum