let r, x0 be Real; :: thesis: ( 0 < r implies ].(x0 - r),(x0 + r).[ \ {x0} = ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ )
assume A1: 0 < r ; :: thesis: ].(x0 - r),(x0 + r).[ \ {x0} = ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[
thus ].(x0 - r),(x0 + r).[ \ {x0} c= ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ :: according to XBOOLE_0:def 10 :: thesis: ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= ].(x0 - r),(x0 + r).[ \ {x0}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ].(x0 - r),(x0 + r).[ \ {x0} or x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ )
assume A2: x in ].(x0 - r),(x0 + r).[ \ {x0} ; :: thesis: x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[
then A3: ( x in ].(x0 - r),(x0 + r).[ & not x in {x0} ) by XBOOLE_0:def 5;
consider r1 being Real such that
A4: r1 = x by A2;
A5: r1 <> x0 by A3, A4, TARSKI:def 1;
x in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) } by A3, RCOMP_1:def 2;
then A6: ex g2 being Real st
( g2 = x & x0 - r < g2 & g2 < x0 + r ) ;

now

per cases ( r1 < x0 or x0 < r1 ) by A5, XXREAL_0:1;

suppose r1 < x0 ; :: thesis: x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[

then r1 in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 ) } by A4, A6;
then x in ].(x0 - r),x0.[ by A4, RCOMP_1:def 2;
hence x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x0 < r1 ; :: thesis: x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[

then r1 in { g1 where g1 is Real : ( x0 < g1 & g1 < x0 + r ) } by A4, A6;
then x in ].x0,(x0 + r).[ by A4, RCOMP_1:def 2;
hence x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ or x in ].(x0 - r),(x0 + r).[ \ {x0} )
assume A7: x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ ; :: thesis: x in ].(x0 - r),(x0 + r).[ \ {x0}

now

per cases ( x in ].(x0 - r),x0.[ or x in ].x0,(x0 + r).[ ) by A7, XBOOLE_0:def 3;

suppose x in ].(x0 - r),x0.[ ; :: thesis: x in ].(x0 - r),(x0 + r).[ \ {x0}

then x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 ) } by RCOMP_1:def 2;
then consider g1 being Real such that
A8: ( g1 = x & x0 - r < g1 & g1 < x0 ) ;
A9: not x in {x0} by A8, TARSKI:def 1;
g1 < x0 + r by A1, A8, Lm1;
then x in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) } by A8;
then x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
hence x in ].(x0 - r),(x0 + r).[ \ {x0} by A9, XBOOLE_0:def 5; :: thesis: verum

end;

suppose x in ].x0,(x0 + r).[ ; :: thesis: x in ].(x0 - r),(x0 + r).[ \ {x0}

then x in { g1 where g1 is Real : ( x0 < g1 & g1 < x0 + r ) } by RCOMP_1:def 2;
then consider g1 being Real such that
A10: ( g1 = x & x0 < g1 & g1 < x0 + r ) ;
A11: not x in {x0} by A10, TARSKI:def 1;
x0 - r < g1 by A1, A10, Lm1;
then x in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) } by A10;
then x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
hence x in ].(x0 - r),(x0 + r).[ \ {x0} by A11, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

hence x in ].(x0 - r),(x0 + r).[ \ {x0} ; :: thesis: verum