let a, b be Real; :: thesis: for A being Subset of R^1 st A = [.a,b.] holds
A is closed
let A be Subset of R^1; :: thesis: ( A = [.a,b.] implies A is closed )
assume A1: A = [.a,b.] ; :: thesis: A is closed
reconsider B = A ` as Subset of (TopSpaceMetr RealSpace) by TOPMETR:def 6;
reconsider a = a, b = b as Real ;
reconsider D = B as Subset of RealSpace by TOPMETR:12;
set C = D ` ;
A2: the carrier of RealSpace = the carrier of (TopSpaceMetr RealSpace) by TOPMETR:12;
for c being Point of RealSpace st c in B holds
ex r being Real st
( r > 0 & Ball (c,r) c= B )

proof

let c be Point of RealSpace; :: thesis: ( c in B implies ex r being Real st
( r > 0 & Ball (c,r) c= B ) )
reconsider n = c as Element of REAL by METRIC_1:def 13;
assume c in B ; :: thesis: ex r being Real st
( r > 0 & Ball (c,r) c= B )
then not n in [.a,b.] by A1, XBOOLE_0:def 5;
then A3: not n in { p where p is Real : ( a <= p & p <= b ) } by RCOMP_1:def 1;

now :: thesis: ex r being set st
( r > 0 & Ball (c,r) c= B )

per cases ( not a <= n or not n <= b ) by A3;

suppose A4: not a <= n ; :: thesis: ex r being set st
( r > 0 & Ball (c,r) c= B )

take r = a - n; :: thesis: ( r > 0 & Ball (c,r) c= B )

now :: thesis: for x being object st x in Ball (c,r) holds
x in B

let x be object ; :: thesis: ( x in Ball (c,r) implies x in B )
assume A5: x in Ball (c,r) ; :: thesis: x in B
then reconsider t = x as Element of REAL by METRIC_1:def 13;
reconsider u = x as Point of RealSpace by A5;
Ball (c,r) = { q where q is Element of RealSpace : dist (c,q) < r } by METRIC_1:17;
then ex v being Element of RealSpace st
( v = u & dist (c,v) < r ) by A5;
then real_dist . (t,n) < r by METRIC_1:def 1, METRIC_1:def 13;
then A6: |.(t - n).| < r by METRIC_1:def 12;
t - n <= |.(t - n).| by ABSVALUE:4;
then t - n < a - n by A6, XXREAL_0:2;
then for q being Real holds
( not q = t or not a <= q or not q <= b ) by XREAL_1:9;
then not t in { p where p is Real : ( a <= p & p <= b ) } ;
then not u in D ` by A1, A2, RCOMP_1:def 1, TOPMETR:def 6;
hence x in B by SUBSET_1:29; :: thesis: verum

end;

hence ( r > 0 & Ball (c,r) c= B ) by A4, XREAL_1:50; :: thesis: verum

end;

suppose A7: not n <= b ; :: thesis: ex r being set st
( r > 0 & Ball (c,r) c= B )

take r = n - b; :: thesis: ( r > 0 & Ball (c,r) c= B )

now :: thesis: for x being object st x in Ball (c,r) holds
x in B

let x be object ; :: thesis: ( x in Ball (c,r) implies x in B )
assume A8: x in Ball (c,r) ; :: thesis: x in B
then reconsider t = x as Element of REAL by METRIC_1:def 13;
reconsider u = x as Point of RealSpace by A8;
Ball (c,r) = { q where q is Element of RealSpace : dist (c,q) < r } by METRIC_1:17;
then ex v being Element of RealSpace st
( v = u & dist (c,v) < r ) by A8;
then real_dist . (n,t) < r by METRIC_1:def 1, METRIC_1:def 13;
then A9: |.(n - t).| < r by METRIC_1:def 12;
n - t <= |.(n - t).| by ABSVALUE:4;
then n - t < n - b by A9, XXREAL_0:2;
then for q being Real holds
( not q = t or not a <= q or not q <= b ) by XREAL_1:10;
then not t in { p where p is Real : ( a <= p & p <= b ) } ;
then not u in D ` by A1, A2, RCOMP_1:def 1, TOPMETR:def 6;
hence x in B by SUBSET_1:29; :: thesis: verum

end;

hence ( r > 0 & Ball (c,r) c= B ) by A7, XREAL_1:50; :: thesis: verum

end;

end;

end;

hence ex r being Real st
( r > 0 & Ball (c,r) c= B ) ; :: thesis: verum

end;

then A ` is open by TOPMETR:15, TOPMETR:def 6;
hence A is closed by TOPS_1:3; :: thesis: verum