let B be Subset of R^1; :: thesis: ( B = NAT implies B is closed )

A1: dom (id NAT) = NAT ;

A2: rng (id NAT) = NAT ;

then reconsider S = id NAT as sequence of R^1 by A1, FUNCT_2:2, TOPMETR:17, NUMBERS:19;

for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[

A1: dom (id NAT) = NAT ;

A2: rng (id NAT) = NAT ;

then reconsider S = id NAT as sequence of R^1 by A1, FUNCT_2:2, TOPMETR:17, NUMBERS:19;

for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[

proof

hence
( B = NAT implies B is closed )
by A2, Th9; :: thesis: verum
let n be Element of NAT ; :: thesis: S . n in ].(n - (1 / 4)),(n + (1 / 4)).[

reconsider x = S . n as Real ;

A3: (- (1 / 4)) + n < 0 + n by XREAL_1:8;

( x = n & n < n + (1 / 4) ) by XREAL_1:29;

then x in { r where r is Real : ( n - (1 / 4) < r & r < n + (1 / 4) ) } by A3;

hence S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ by RCOMP_1:def 2; :: thesis: verum

end;reconsider x = S . n as Real ;

A3: (- (1 / 4)) + n < 0 + n by XREAL_1:8;

( x = n & n < n + (1 / 4) ) by XREAL_1:29;

then x in { r where r is Real : ( n - (1 / 4) < r & r < n + (1 / 4) ) } by A3;

hence S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ by RCOMP_1:def 2; :: thesis: verum