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:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A3: x in [#] I[01] ; :: thesis:
reconsider p = x as Point of RealSpace by A3, BORSUK_1:40;

let r be Real; :: thesis:
assume A4: r > 0 ; :: thesis:
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;

suppose r <= p ; :: thesis:

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:

end;

suppose r > p ; :: thesis:

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:

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: