let B be Subset of R^1 ; :: thesis: ( B = NAT implies B is closed )
A1: dom (id NAT ) = NAT by FUNCT_1:34;
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:34;
hence y in rng (id NAT ) by A1, A3, FUNCT_1:def 5; :: thesis: verum

end;

then reconsider S = id NAT as sequence of R^1 by A1, FUNCT_2:4, TOPMETR:24;
A4: 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:34;
A5: (- (1 / 4)) + n < 0 + n by XREAL_1:10;
( x = n & n < n + (1 / 4) ) by FUNCT_1:34, XREAL_1:31;
then x in { r where r is Real : ( n - (1 / 4) < r & r < n + (1 / 4) ) } by A5;
hence S . n in ].(n - (1 / 4)),(n + (1 / 4)).[ by RCOMP_1:def 2; :: thesis: verum

end;

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