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;

hence x in Cl D by A3, A2, BORSUK_1:40, XBOOLE_0:def 4; :: thesis: verum

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

then
x in Cl (Up D1)
by GOBOARD6:92, TOPMETR:def 6;Ball (p,r) meets D

let r be Real; :: thesis: ( r > 0 implies Ball (p,b_{1}) meets D )

assume A4: r > 0 ; :: thesis: Ball (p,b_{1}) 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;

end;assume A4: r > 0 ; :: thesis: Ball (p,b

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 )
;

end;

suppose
r <= p
; :: thesis: Ball (p,b_{1}) 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;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

suppose
r > p
; :: thesis: Ball (p,b_{1}) 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;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

hence x in Cl D by A3, A2, BORSUK_1:40, XBOOLE_0:def 4; :: thesis: verum