let r, s be Real; :: thesis: for jauge being Function of [.r,s.],].0,+infty.[
for S being Subset-Family of (Closed-Interval-TSpace (r,s)) st r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
S is open
let jauge be Function of [.r,s.],].0,+infty.[; :: thesis: for S being Subset-Family of (Closed-Interval-TSpace (r,s)) st r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
S is open
let S be Subset-Family of (Closed-Interval-TSpace (r,s)); :: thesis: ( r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } implies S is open )
assume that
A1: r <= s and
A2: S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } ; :: thesis: S is open
for P being Subset of (Closed-Interval-TSpace (r,s)) st P in S holds
P is open

proof

let P be Subset of (Closed-Interval-TSpace (r,s)); :: thesis: ( P in S implies P is open )
assume P in S ; :: thesis: P is open
then consider x0 being Element of [.r,s.] such that
A4: P = ].(x0 - (jauge . x0)),(x0 + (jauge . x0)).[ /\ [.r,s.] by A2;
set CIT = Closed-Interval-TSpace (r,s);
set CIM = Closed-Interval-MSpace (r,s);
A5: Closed-Interval-TSpace (r,s) = TopSpaceMetr (Closed-Interval-MSpace (r,s)) by TOPMETR:def 7;
A6: TopSpaceMetr (Closed-Interval-MSpace (r,s)) = TopStruct(# the carrier of (Closed-Interval-MSpace (r,s)),(Family_open_set (Closed-Interval-MSpace (r,s))) #) by PCOMPS_1:def 5;
reconsider I = [.r,s.] as non empty Subset of RealSpace by A1, XXREAL_1:30;
reconsider P1 = P as Subset of (Closed-Interval-MSpace (r,s)) by TOPMETR:def 7, A6;
for t being Element of (Closed-Interval-MSpace (r,s)) st t in P1 holds
ex r being Real st
( r > 0 & Ball (t,r) c= P1 )

proof

let t be Element of (Closed-Interval-MSpace (r,s)); :: thesis: ( t in P1 implies ex r being Real st
( r > 0 & Ball (t,r) c= P1 ) )
assume A7: t in P1 ; :: thesis: ex r being Real st
( r > 0 & Ball (t,r) c= P1 )
the carrier of (Closed-Interval-MSpace (r,s)) c= the carrier of RealSpace by TOPMETR:def 1;
then reconsider tr = t as Point of RealSpace ;
reconsider XJ = ].(x0 - (jauge . x0)),(x0 + (jauge . x0)).[ as Subset of RealSpace ;
reconsider XK = XJ as Subset of R^1 by TOPMETR:17;
not [.r,s.] is empty by A1, XXREAL_1:30;
then x0 in [.r,s.] ;
then reconsider p = x0 as Point of RealSpace ;
tr in XK by A7, A4, XBOOLE_0:def 4;
then consider r0 being Real such that
A8: r0 > 0 and
A9: Ball (tr,r0) c= XK by JORDAN6:35, TOPMETR:15, TOPMETR:def 6;
take r0 ; :: thesis: ( r0 > 0 & Ball (t,r0) c= P1 )
Ball (t,r0) = (Ball (tr,r0)) /\ the carrier of (Closed-Interval-MSpace (r,s)) by TOPMETR:9;
then Ball (t,r0) = (Ball (tr,r0)) /\ [.r,s.] by A1, TOPMETR:10;
hence ( r0 > 0 & Ball (t,r0) c= P1 ) by A4, A8, A9, XBOOLE_1:27; :: thesis: verum

end;

then P in Family_open_set (Closed-Interval-MSpace (r,s)) by PCOMPS_1:def 4;
hence P is open by A5, A6, PRE_TOPC:def 2; :: thesis: verum

end;

hence S is open by TOPS_2:def 1; :: thesis: verum