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 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 ;

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:12;
(Ball (x,(1 / 4))) /\ ((B `) `) = {} by A3, Th7;
then C misses (B `) ` ;
then Ball (x,(1 / 4)) c= B ` by SUBSET_1:24;
hence ex r being Real st
( r > 0 & Ball (x,r) c= B ` ) ; :: thesis:

end;

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

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

proof

assume Ball (x,|.(x1 - y).|) meets rng S ; :: thesis:
then consider z being object such that
A10: z in Ball (x,|.(x1 - y).|) and
A11: z in rng S by XBOOLE_0:3;
consider n2 being object such that
A12: n2 in dom S and
A13: z = S . n2 by A11, FUNCT_1:def 3;
reconsider n2 = n2 as Element of NAT by A12;
reconsider z = z as Real by A10;

per cases by XXREAL_0:1;

suppose A14: n1 = n2 ; :: thesis:

A15: |.(x1 - y).| = |.(0 + (- (y - x1))).|
.= |.(y - x1).| by COMPLEX1:52 ;
y in ].(x1 - |.(x1 - y).|),(x1 + |.(x1 - y).|).[ by A8, A10, A13, A14, Th7;
hence contradiction by A15, RCOMP_1:1; :: 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:19;
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:19;
then A18: n2 + 1 > (z - (1 / 4)) + 1 by XREAL_1:6;
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:20;
Ball (x,|.(x1 - y).|) 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:19;
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:9;
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:6;
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:6;
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:9;
then A23: n1 + 1 > (y - (1 / 4)) + 1 by XREAL_1:6;
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:9;
Ball (x,|.(x1 - y).|) 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:19;
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:6;
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:6;
then z - (1 / 2) < (y + (1 / 2)) - (1 / 2) by XREAL_1:9;
hence contradiction by A24; :: thesis:

end;

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

proof

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

end;

then x1 + (- y) <> y + (- y) ;
then |.(x1 - y).| > 0 by COMPLEX1:47;
hence ex r being Real st
( r > 0 & Ball (x,r) c= B ` ) by A26; :: thesis:

end;

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