I want to prove that $\vdash\phi\rightarrow\neg\Box\neg\phi$ is a theorem in S5
I have S5 definition :
\begin{align*} T&:\Box p\rightarrow p\\ 5&:\Diamond p\rightarrow \Box\Diamond p\\ K&:\Box (p\rightarrow q)\rightarrow(\Box p\rightarrow \Box \phi)\\ Nec&:\frac{\phi}{\Box\phi} \end{align*}
And theorem definition :
A formula is a theorem of S5 $\Leftrightarrow\phi$ is valid in all frames where R is an equivalence relation
\begin{align} &\neg (\phi\rightarrow\neg\Box\neg\phi),w_i\mbox{ as an hypothesis}\\ &\phi,w_i \mbox{ from }R_\neg \mbox{ on } 1\\ &\Diamond\phi,w_i\mbox{ from }R_\neg \mbox{ on } 1\\ \end{align}
I'm not sure I have here an equivalence relation to conclude that
Therefore $\phi$ is valid in all frames and $\vdash\phi\rightarrow\neg\Box\neg\phi$ is a theorem in S5
Third attempt
\begin{align} \neg\phi\rightarrow\Box\neg\phi,w_i \mbox{ contrapositive of }T\\ \neg\neg\phi\rightarrow\neg\Box\neg\phi,w_i \mbox{ negation of }1 \end{align}
Therefore $\phi$ is valid and $\vdash\phi\rightarrow\neg\Box\neg\phi$ is a theorem in S5