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

end;

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

end;

hence B is closed by A1, A3, Th9; :: thesis: verum