Negative introspection axiom and Euclidean property of accessibility relation Revising the modal logic principles, I have encountered an negative introspection axiom:
$$ \vDash \neg \square \alpha \longrightarrow \square \neg \square \alpha $$
with additional information, that it is a direct effect from Euclidean property of accessibility relation $\mathbb{R}$. Square operator is defined as follows (for Kripke structure $\kappa = (\mathbb{W}, \mathbb{R}, m)$):
$$ \kappa, w \vDash \square \alpha \equiv \forall w' \in \mathbb{W} \quad w\mathbb{R}w' \implies \kappa, w' \vDash \alpha $$
I got stuck in the point where I have to apply the Euclidean property. We basically know that for any Kripke structure $\kappa$ and state $w \in \mathbb{W}$:
$$ \exists w' \in \mathbb{W} \quad w\mathbb{R}w' \wedge \kappa, w' \nvDash \alpha$$
and from the fact that $\mathbb{R}$ is Euclidean:
$$ \forall w_{1}, w_{2}, w_{3} \in \mathbb{W} \quad w_{1}\mathbb{R}w_{2} \wedge w_{1}\mathbb{R}w_{3} \implies w_{2}\mathbb{R}w_{3} $$
I've tried to make it similarily to this, but there we have all universal quantifiers, so it was moreorless sensible to me. I would be really grateful, if someone would provide a solution or any hint to that. 
 A: This is the same thing as $\lozenge \alpha\to \square\lozenge \alpha.$ If $\lozenge \alpha$ holds, then there is some accessible world at which $\alpha$ holds. By the Euclidean property, that world is accessible from every accessible world, so $\lozenge\alpha$ holds at every accessible world. In other words, $\square \lozenge \alpha$ holds.
A: By the time, I have found a possible solution, I would appreciate some comments:
Let's get any possible world $w \in \mathbb{W}$, such as $\kappa, w \vDash \neg \square \alpha $. Then,from a definition of $\square$:
$$ \exists w' \in \mathbb{B} w\mathbb{R}w' \wedge \kappa, w' \vDash \neg \alpha $$
Let's consider any state $w'' \in \mathbb{W}$ such as $w\mathbb{R}w''$. Then, from Euclideanity of $\mathbb{R}$ we have $w\mathbb{R}w'' \wedge w\mathbb{R}w' \implies w''\mathbb{R}w'$. That concludes to the following:
$$\forall w'' \in \mathbb{W} \, \exists w' \in \mathbb{W} \, w\mathbb{R}w'' \implies  w''\mathbb{R}w' \wedge \kappa, w' \vDash \neg \alpha $$
which is equivalent to:
$$ \forall w'' \in \mathbb{W} \,, w\mathbb{R}w'' \implies \kappa, w'' \vDash \neg \square \alpha$$
and is in fact a definition of $\square$ operator: $\kappa, w \vDash \square \neg \square \alpha$. To sum up, for any Kripke structure $\kappa$ and state $w \in \mathbb{W}$ we have $\kappa, w \vDash \neg \square \alpha \implies \kappa, w \vDash \square \neg \square \alpha$, thus thesis: $\vDash \neg \square \alpha \longrightarrow\square \neg \square \alpha$. $\blacksquare$
