reconsider P = [.0,1.] as Subset of R^1 by MEMBERED:3, TOPMETR:17;
A1: I[01] = R^1 | P by TOPMETR:19, TOPMETR:20;
reconsider D1 = D as Subset of (R^1 | P) by TOPMETR:19, TOPMETR:20;
A2: Cl D = (Cl (Up D1)) /\ P by A1, CONNSP_3:30;
thus Cl D c= [#] I[01] ; :: according to XBOOLE_0:def 10 :: thesis: [#] I[01] c= Cl D
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] I[01] or x in Cl D )
assume A3: x in [#] I[01] ; :: thesis: x in Cl D
reconsider p = x as Point of RealSpace by A3, BORSUK_1:40;

now :: thesis: for r being Real st r > 0 holds
Ball (p,r) meets D

let r be Real; :: thesis: ( r > 0 implies Ball (p,b₁) meets D )
assume A4: r > 0 ; :: thesis: Ball (p,b₁) meets D
A5: p - r < p - 0 by A4, XREAL_1:10;
A6: p <= 1 by A3, BORSUK_1:43;
A7: Ball (p,r) = ].(p - r),(p + r).[ by FRECHET:7;

per cases ( r <= p or r > p ) ;

suppose r <= p ; :: thesis: Ball (p,b₁) meets D

then r - r <= p - r by XREAL_1:9;
then consider c being Real such that
A8: c in D and
A9: p - r < c and
A10: c < p by A5, A6, URYSOHN2:24;
p + 0 < p + r by A4, XREAL_1:8;
then c < p + r by A10, XXREAL_0:2;
then c in Ball (p,r) by A9, A7, XXREAL_1:4;
hence Ball (p,r) meets D by A8, XBOOLE_0:3; :: thesis: verum

end;

suppose r > p ; :: thesis: Ball (p,b₁) meets D

then A11: p - r < p - p by XREAL_1:10;
0 <= p by A3, BORSUK_1:43;
then 0 in Ball (p,r) by A4, A11, A7, XXREAL_1:4;
hence Ball (p,r) meets D by URYSOHN2:27, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

then x in Cl (Up D1) by GOBOARD6:92, TOPMETR:def 6;
hence x in Cl D by A3, A2, BORSUK_1:40, XBOOLE_0:def 4; :: thesis: verum