let a, b be real number ; :: 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 7;
reconsider a = a, b = b as Real by XREAL_0:def 1;
reconsider D = B as Subset of RealSpace by TOPMETR:16;
set C = D ` ;
A2: the carrier of RealSpace = the carrier of (TopSpaceMetr RealSpace ) by TOPMETR:16;
for c being Point of RealSpace st c in B holds
ex r being real number st
( r > 0 & Ball c,r c= B )

proof

let c be Point of RealSpace ; :: thesis: ( c in B implies ex r being real number st
( r > 0 & Ball c,r c= B ) )
reconsider n = c as Real by METRIC_1:def 14;
assume c in B ; :: thesis: ex r being real number 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

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

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

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

now

let x be set ; :: 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 Real by METRIC_1:def 14;
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:18;
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 14;
then A6: abs (t - n) < r by METRIC_1:def 13;
t - n <= abs (t - n) by ABSVALUE:11;
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:11;
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 7;
hence x in B by SUBSET_1:50; :: thesis: verum

end;

hence ( r > 0 & Ball c,r c= B ) by A4, TARSKI:def 3, XREAL_1:52; :: thesis: verum

end;

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

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

now

let x be set ; :: 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 Real by METRIC_1:def 14;
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:18;
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 14;
then A9: abs (n - t) < r by METRIC_1:def 13;
n - t <= abs (n - t) by ABSVALUE:11;
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:12;
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 7;
hence x in B by SUBSET_1:50; :: thesis: verum

end;

hence ( r > 0 & Ball c,r c= B ) by A7, TARSKI:def 3, XREAL_1:52; :: thesis: verum

end;

end;

end;

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

end;

then A ` is open by TOPMETR:22, TOPMETR:def 7;
hence A is closed by TOPS_1:29; :: thesis: verum