let S be sequence of R^1 ; :: thesis:
reconsider B = rng S as Subset of R^1 ;
assume A1: for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ ; :: thesis:
for x being Point of RealSpace st x in B ` holds
ex r being real number st
( r > 0 & Ball x,r c= B ` )

proof

let x be Point of RealSpace ; :: thesis:
assume A2: x in B ` ; :: thesis:
reconsider x1 = x as Real by METRIC_1:def 14;

per cases /\ B = {} or ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B <> {} ) ;

suppose A3: ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B = {} ; :: thesis:

reconsider C = Ball x,(1 / 4) as Subset of R^1 by TOPMETR:16;
(Ball x,(1 / 4)) /\ ((B ` ) ` ) = {} by A3, Th7;
then C misses (B ` ) ` by XBOOLE_0:def 7;
then Ball x,(1 / 4) c= B ` by SUBSET_1:44;
hence ex r being real number st
( r > 0 & Ball x,r c= B ` ) ; :: thesis:

end;

suppose A4: ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B <> {} ; :: thesis:

consider y being Element of ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ /\ B;
A5: y in ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ by A4, XBOOLE_0:def 4;
A6: y in B by A4, XBOOLE_0:def 4;
reconsider y = y as Real by A5;
consider n1 being set such that
A7: n1 in dom S and
A8: y = S . n1 by A6, FUNCT_1:def 5;
reconsider n1 = n1 as Element of NAT by A7;
reconsider r = abs (x1 - y) as Real ;
reconsider C = Ball x,r as Subset of R^1 by TOPMETR:16;
abs (y - x1) < 1 / 4 by A5, RCOMP_1:8;
then abs (- (x1 - y)) < 1 / 4 ;
then A9: r <= 1 / 4 by COMPLEX1:138;
Ball x,r misses rng S

proof

assume Ball x,r meets rng S ; :: thesis:
then consider z being set such that
A10: z in Ball x,r and
A11: z in rng S by XBOOLE_0:3;
consider n2 being set such that
A12: n2 in dom S and
A13: z = S . n2 by A11, FUNCT_1:def 5;
reconsider n2 = n2 as Element of NAT by A12;
reconsider z = z as Real by A10, METRIC_1:def 14;

per cases by XXREAL_0:1;

suppose A14: n1 = n2 ; :: thesis:

A15: r = abs (0 + (- (y - x1)))
.= abs (y - x1) by COMPLEX1:138 ;
y in ].(x1 - r),(x1 + r).[ by A8, A10, A13, A14, Th7;
hence contradiction by A15, RCOMP_1:8; :: thesis:

end;

suppose A16: n1 > n2 ; :: thesis:

S . n1 in ].(n1 - (1 / 4)),(n1 + (1 / 4)).[ by A1;
then S . n1 in { a where a is Real : ( n1 - (1 / 4) < a & a < n1 + (1 / 4) ) } by RCOMP_1:def 2;
then ex a1 being Real st
( S . n1 = a1 & n1 - (1 / 4) < a1 & a1 < n1 + (1 / 4) ) ;
then A17: n1 < y + (1 / 4) by A8, XREAL_1:21;
S . n2 in ].(n2 - (1 / 4)),(n2 + (1 / 4)).[ by A1;
then S . n2 in { a where a is Real : ( n2 - (1 / 4) < a & a < n2 + (1 / 4) ) } by RCOMP_1:def 2;
then ex a2 being Real st
( S . n2 = a2 & n2 - (1 / 4) < a2 & a2 < n2 + (1 / 4) ) ;
then z - (1 / 4) < n2 by A13, XREAL_1:21;
then A18: n2 + 1 > (z - (1 / 4)) + 1 by XREAL_1:8;
n2 + 1 <= n1 by A16, NAT_1:13;
then n2 + 1 < y + (1 / 4) by A17, XXREAL_0:2;
then z + ((- (1 / 4)) + 1) < y + (1 / 4) by A18, XXREAL_0:2;
then A19: z < (y + (1 / 4)) - ((- (1 / 4)) + 1) by XREAL_1:22;
Ball x,r c= Ball x,(1 / 4) by A9, PCOMPS_1:1;
then z in Ball x,(1 / 4) by A10;
then z in ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ by Th7;
then z in { a where a is Real : ( x1 - (1 / 4) < a & a < x1 + (1 / 4) ) } by RCOMP_1:def 2;
then ex a1 being Real st
( a1 = z & x1 - (1 / 4) < a1 & a1 < x1 + (1 / 4) ) ;
then A20: z + (1 / 4) > x1 by XREAL_1:21;
y in { a where a is Real : ( x1 - (1 / 4) < a & a < x1 + (1 / 4) ) } by A5, RCOMP_1:def 2;
then ex a1 being Real st
( y = a1 & x1 - (1 / 4) < a1 & a1 < x1 + (1 / 4) ) ;
then y - (1 / 4) < (x1 + (1 / 4)) - (1 / 4) by XREAL_1:11;
then z + (1 / 4) > y - (1 / 4) by A20, XXREAL_0:2;
then (z + (1 / 4)) + (- (1 / 4)) > (y - (1 / 4)) + (- (1 / 4)) by XREAL_1:8;
hence contradiction by A19; :: thesis:

end;

suppose A21: n1 < n2 ; :: thesis:

S . n2 in ].(n2 - (1 / 4)),(n2 + (1 / 4)).[ by A1;
then S . n2 in { a where a is Real : ( n2 - (1 / 4) < a & a < n2 + (1 / 4) ) } by RCOMP_1:def 2;
then ex a2 being Real st
( S . n2 = a2 & n2 - (1 / 4) < a2 & a2 < n2 + (1 / 4) ) ;
then A22: z + (1 / 4) > (n2 + (- (1 / 4))) + (1 / 4) by A13, XREAL_1:8;
S . n1 in ].(n1 - (1 / 4)),(n1 + (1 / 4)).[ by A1;
then S . n1 in { a where a is Real : ( n1 - (1 / 4) < a & a < n1 + (1 / 4) ) } by RCOMP_1:def 2;
then ex a1 being Real st
( S . n1 = a1 & n1 - (1 / 4) < a1 & a1 < n1 + (1 / 4) ) ;
then (n1 + (1 / 4)) - (1 / 4) > y - (1 / 4) by A8, XREAL_1:11;
then A23: n1 + 1 > (y - (1 / 4)) + 1 by XREAL_1:8;
n1 + 1 <= n2 by A21, NAT_1:13;
then z + (1 / 4) > n1 + 1 by A22, XXREAL_0:2;
then (y + (- (1 / 4))) + 1 < z + (1 / 4) by A23, XXREAL_0:2;
then A24: (y + ((- (1 / 4)) + 1)) - ((- (1 / 4)) + 1) < (z + (1 / 4)) - ((- (1 / 4)) + 1) by XREAL_1:11;
Ball x,r c= Ball x,(1 / 4) by A9, PCOMPS_1:1;
then z in Ball x,(1 / 4) by A10;
then z in ].(x1 - (1 / 4)),(x1 + (1 / 4)).[ by Th7;
then z in { a where a is Real : ( x1 - (1 / 4) < a & a < x1 + (1 / 4) ) } by RCOMP_1:def 2;
then ex a1 being Real st
( a1 = z & x1 - (1 / 4) < a1 & a1 < x1 + (1 / 4) ) ;
then A25: z - (1 / 4) < x1 by XREAL_1:21;
y in { a where a is Real : ( x1 - (1 / 4) < a & a < x1 + (1 / 4) ) } by A5, RCOMP_1:def 2;
then ex a1 being Real st
( y = a1 & x1 - (1 / 4) < a1 & a1 < x1 + (1 / 4) ) ;
then (x1 + (- (1 / 4))) + (1 / 4) < y + (1 / 4) by XREAL_1:8;
then z - (1 / 4) < y + (1 / 4) by A25, XXREAL_0:2;
then (z - (1 / 4)) + (1 / 4) < (y + (1 / 4)) + (1 / 4) by XREAL_1:8;
then z - (1 / 2) < (y + (1 / 2)) - (1 / 2) by XREAL_1:11;
hence contradiction by A24; :: thesis:

end;

then C misses (B ` ) ` ;
then A26: C c= B ` by SUBSET_1:44;
x1 <> y

proof

assume x1 = y ; :: thesis:
then y in B /\ (B ` ) by A2, A6, XBOOLE_0:def 4;
then B meets B ` by XBOOLE_0:4;
hence contradiction by SUBSET_1:44; :: thesis:

end;

then x1 + (- y) <> y + (- y) ;
then abs (x1 - y) > 0 by COMPLEX1:133;
hence ex r being real number st
( r > 0 & Ball x,r c= B ` ) by A26; :: thesis:

end;

then ([#] R^1 ) \ (rng S) is open by TOPMETR:22;
hence rng S is closed by PRE_TOPC:def 6; :: thesis: