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 object ; :: 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 consider r1 being Real such that
A3: r1 = x ;
x in ].(x0 - r),(x0 + r).[ by A2, XBOOLE_0:def 5;
then x in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) } by RCOMP_1:def 2;
then A4: ex g2 being Real st
( g2 = x & x0 - r < g2 & g2 < x0 + r ) ;
not x in {x0} by A2, XBOOLE_0:def 5;
then A5: r1 <> x0 by A3, TARSKI:def 1;

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

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 A3, A4;
then x in ].(x0 - r),x0.[ by A3, 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 A3, A4;
then x in ].x0,(x0 + r).[ by A3, 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ or x in ].(x0 - r),(x0 + r).[ \ {x0} )
assume A6: x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ ; :: thesis: x in ].(x0 - r),(x0 + r).[ \ {x0}

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

per cases ( x in ].(x0 - r),x0.[ or x in ].x0,(x0 + r).[ ) by A6, 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
A7: g1 = x and
A8: x0 - r < g1 and
A9: g1 < x0 ;
g1 < x0 + r by A1, A9, Lm1;
then x in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) } by A7, A8;
then A10: x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
not x in {x0} by A7, A9, TARSKI:def 1;
hence x in ].(x0 - r),(x0 + r).[ \ {x0} by A10, 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
A11: g1 = x and
A12: x0 < g1 and
A13: g1 < x0 + r ;
x0 - r < g1 by A1, A12, Lm1;
then x in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) } by A11, A13;
then A14: x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
not x in {x0} by A11, A12, TARSKI:def 1;
hence x in ].(x0 - r),(x0 + r).[ \ {x0} by A14, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

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