let S be sequence of R^1; :: thesis: ( ( for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ ) implies rng S is closed )

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: rng S is closed

for x being Point of RealSpace st x in B ` holds

ex r being Real st

( r > 0 & Ball (x,r) c= B ` )

hence rng S is closed by PRE_TOPC:def 3; :: thesis: verum

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: rng S is closed

for x being Point of RealSpace st x in B ` holds

ex r being Real st

( r > 0 & Ball (x,r) c= B ` )

proof

then
([#] R^1) \ (rng S) is open
by TOPMETR:15;
let x be Point of RealSpace; :: thesis: ( x in B ` implies ex r being Real st

( r > 0 & Ball (x,r) c= B ` ) )

assume A2: x in B ` ; :: thesis: ex r being Real st

( r > 0 & Ball (x,r) c= B ` )

reconsider x1 = x as Real ;

end;( r > 0 & Ball (x,r) c= B ` ) )

assume A2: x in B ` ; :: thesis: ex r being Real st

( r > 0 & Ball (x,r) c= B ` )

reconsider x1 = x as Real ;

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

end;

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

( r > 0 & Ball (x,r) c= B ` )

( r > 0 & Ball (x,r) c= B ` )

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: verum

end;(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: verum

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

( r > 0 & Ball (x,r) c= B ` )

( r > 0 & Ball (x,r) c= B ` )

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

then A26: C c= B ` by SUBSET_1:24;

x1 <> y

then |.(x1 - y).| > 0 by COMPLEX1:47;

hence ex r being Real st

( r > 0 & Ball (x,r) c= B ` ) by A26; :: thesis: verum

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

then
C misses (B `) `
;
assume
Ball (x,|.(x1 - y).|) meets rng S
; :: thesis: contradiction

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;

end;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
( n1 = n2 or n1 > n2 or n1 < n2 )
by XXREAL_0:1;

end;

suppose A14:
n1 = n2
; :: thesis: contradiction

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: verum

end;.= |.(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: verum

suppose A16:
n1 > n2
; :: thesis: contradiction

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: verum

end;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: verum

suppose A21:
n1 < n2
; :: thesis: contradiction

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: verum

end;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: verum

then A26: C c= B ` by SUBSET_1:24;

x1 <> y

proof

then
x1 + (- y) <> y + (- y)
;
assume
x1 = y
; :: thesis: contradiction

then y in B /\ (B `) by A2, A6, XBOOLE_0:def 4;

then B meets B ` ;

hence contradiction by SUBSET_1:24; :: thesis: verum

end;then y in B /\ (B `) by A2, A6, XBOOLE_0:def 4;

then B meets B ` ;

hence contradiction by SUBSET_1:24; :: thesis: verum

then |.(x1 - y).| > 0 by COMPLEX1:47;

hence ex r being Real st

( r > 0 & Ball (x,r) c= B ` ) by A26; :: thesis: verum

hence rng S is closed by PRE_TOPC:def 3; :: thesis: verum