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)).[

proof

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;

hence ( B = NAT implies B is closed ) by A2, Th9; :: thesis: verum