reconsider P = [.0,1.] as Subset of R^1 by ;
A1: I = R^1 | P by ;
reconsider D1 = D as Subset of (R^1 | P) by ;
A2: Cl D = (Cl (Up D1)) /\ P by ;
thus Cl D c= [#] I ; :: according to XBOOLE_0:def 10 :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] I or x in Cl D )
assume A3: x in [#] I ; :: thesis: x in Cl D
reconsider p = x as Point of RealSpace by ;
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,b1) meets D )
assume A4: r > 0 ; :: thesis: Ball (p,b1) meets D
A5: p - r < p - 0 by ;
A6: p <= 1 by ;
A7: Ball (p,r) = ].(p - r),(p + r).[ by FRECHET:7;
per cases ( r <= p or r > p ) ;
suppose r <= p ; :: thesis: Ball (p,b1) 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 ;
p + 0 < p + r by ;
then c < p + r by ;
then c in Ball (p,r) by ;
hence Ball (p,r) meets D by ; :: thesis: verum
end;
suppose r > p ; :: thesis: Ball (p,b1) meets D
then A11: p - r < p - p by XREAL_1:10;
0 <= p by ;
then 0 in Ball (p,r) by ;
hence Ball (p,r) meets D by ; :: thesis: verum
end;
end;
end;
then x in Cl (Up D1) by ;
hence x in Cl D by ; :: thesis: verum