theorem Th4: :: LIMFUNC3:4

for r, x0 being Real st 0 < r holds
].(x0 - r),(x0 + r).[ \ {x0} = ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[