let B be Subset of R^1; :: thesis: ( B = NAT implies B is closed )
A1: dom (id NAT) = NAT by FUNCT_1:17;
A2: rng (id NAT) = NAT

proof

thus rng (id NAT) c= NAT ; :: according to XBOOLE_0:def 10 :: thesis: NAT c= rng (id NAT)
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in NAT or y in rng (id NAT) )
assume A3: y in NAT ; :: thesis: y in rng (id NAT)
then (id NAT) . y = y by FUNCT_1:17;
hence y in rng (id NAT) by A1, A3, FUNCT_1:def 3; :: thesis: verum

end;

then reconsider S = id NAT as sequence of R^1 by A1, FUNCT_2:2, TOPMETR:17;
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 by FUNCT_1:17;
A4: (- (1 / 4)) + n < 0 + n by XREAL_1:8;
( x = n & n < n + (1 / 4) ) by FUNCT_1:17, XREAL_1:29;
then x in { r where r is Real : ( n - (1 / 4) < r & r < n + (1 / 4) ) } by A4;
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