So I'm self studying from Schramm's Introduction to Real Analysis book, and I am currently at Chapter 7, on cluster points. I thought that I could use any input regarding improving my technique, whether I got anything wrong and if so where, so all in all any advice is welcome!
The exercise defines the limit superior of an infinite bounded set S by lim sup S = sup S', where S' is the derived set of S. It then asks to show that a = lim sup S iff $(a-\varepsilon,\infty) \cap S$ is infinite for all $\varepsilon\gt0$ and $(a+\varepsilon,\infty) \cap S$ is finite for all $\varepsilon\gt0$.
Now this is my attempt at proving the $\Rightarrow$ part:
Let a = sup S'. Then $\forall\varepsilon\gt0,\exists y\in S'$ such that $a-\varepsilon\lt y$, so $y\in(a-\varepsilon,\infty)$. Letting $\varepsilon' = y-(a-\varepsilon)$, it follows that $(y-\varepsilon',y+\varepsilon')\subseteq(a-\varepsilon,\infty)$ $\Rightarrow$ $(a-\varepsilon,\infty)$ is a neighborhood of y.
But $y\in S'$, so the intersection of S with any neighborhood of y is infinite. Thus $\forall\varepsilon\gt0,(a-\varepsilon,\infty) \cap S$ is infinite.
Now suppose $\exists\varepsilon\gt0$ such that $(a+\varepsilon,\infty) \cap S$ is infinite. Since S is bounded, the intersection is both bounded and infinite. By the Bolzano-Weierstrass Theorem, $(a+\varepsilon,\infty) \cap S$ has a cluster point y. Then $\forall\varepsilon'\gt0, (y-\varepsilon',y+\varepsilon')\cap(a+\varepsilon,\infty)\cap S\setminus ${y}$ \neq \emptyset$.
This implies that $\forall\varepsilon'\gt0,(y-\varepsilon',y+\varepsilon')\cap S\setminus ${y}$ \neq \emptyset$ $\Rightarrow y\in S'$. But a = sup S' $\Rightarrow y\lt a+\varepsilon \Rightarrow a+\varepsilon - y\gt0$. Since $\varepsilon'\gt0$, by the Archimedean property there is a natural number n such that $n(a+\varepsilon-y)\gt\varepsilon'\Rightarrow a+\varepsilon'-y\gt\varepsilon'/n\gt0.$ Letting $\varepsilon'/n=\varepsilon_0'$and rearranging the last inequality we get $\varepsilon_0'+y\lt a+\varepsilon\Rightarrow \exists\varepsilon'\gt0, (y-\varepsilon',y+\varepsilon')\cap (a+\varepsilon,\infty)=\emptyset.$
This implies that y is not a cluster point of $(a+\varepsilon,\infty)\cap S$, which contradicts the beginning of the proof. Thus $\forall\varepsilon\gt0, (a+\varepsilon,\infty)\cap S$ is finite.
Again, any improvement points are more than welcome, I don't really have any place to get feedback from irl. Also, I hope I formatted it properly, it's the first time I'm doing it.