We start with the tautology $A\to((\square\square A\land\square A)\to(\square A\land A))$, which an instance of the schema $X\to((Y\land Z)\to(Z\land X))$. Since $\square(\square A\land A)\leftrightarrow\square\square A\land\square A$ is a theorem in any normal modal logic, $A\to(\square(\square A\land A)\to(\square A\land A))$ is a theorem by the substitution theorem. By the syntactic property RM, $\square A\to\square(\square(\square A\land A)\to(\square A\land A))$ is a theorem. Since $\square(\square(\square A\land A)\to(\square A\land A))\to\square(\square A\land A)$ is an instance of W, by law of syllogism, $\square A\to\square(\square A\land A)$ is a theorem.

Next, from the tautology $\square A\land A\to\square A$, we have the theorem $\square(\square A\land A)\to\square\square A$ by RM. Combining this with the last theorem in the previous paragraph, we see that, by law of syllogism, $\square A\to\square\square A$, or 4, is a theorem. ∎

Suppose first that the schema W is valid in $\mathcal{F}=(U,R)$, then any theorem of GL is valid in $\mathcal{F}$, so in particular 4 is valid in $\mathcal{F}$, and hence $\mathcal{F}$ is transitive (see here). We next show that $R$ is converse well-founded. Suppose not. Then there is a non-empty subset $S\subseteq U$ such that $S$ has no $R$-maximal element. We want to find a model $(U,R,V)$ such that, for some propositional variable $p$ and some world $u$ in $U$, $\not\models_{u}\square(\square p\to p)\to\square p$, or equivalently, $\models_{u}\square(\square p\to p)$ and $\not\models_{u}\square p$. Let $V$ be the valuation such that $V(p):=\{w\in U\mid w\notin S\}$. Pick any $u\in S$. Suppose $uRv$. To show that $\models_{u}\square(\square p\to p)$, we want to show that $\models_{v}\square p\to p$. There are two cases:

• If $v\in S$, then $\not\models_{v}p$. Furthermore, since $S$ does not contain an $R$-maximal element, there is a $w\in S$ such that $vRw$. Since $w\in S$, $\not\models_{w}p$. Since $vRw$, $\not\models_{v}\square p$. As a result, $\models_{v}\square p\to p$.

• If $v\notin S$, then $\models_{v}p$, so that $\models_{v}\square p\to p$.

Next, we want to show that $\not\models_{u}\square p$. Since $u\in S$, and $S$ does not have an $R$-maximal element, there is a $w\in S$ such that $uRw$. Since $w\in S$, $\not\models_{w}p$. But since $uRw$, $\not\models_{u}\square p$.

Conversely, let $\mathcal{F}$ be a transitive and converse well-founded frame, $M$ a model based on $\mathcal{F}$, and $u$ a world in $M$. We want to show that $\models_{u}\square(\square p\to p)\to\square p$. So suppose $\not\models_{u}\square p$. Then the set $S:=\{v\mid uRv\mbox{ and }\not\models_{v}p\}$ is not empty. Since $R$ is converse well-founded, $S$ has a $R$-maximal element, say $w$. So $uRw$ and $\not\models_{w}p$. Now, if $\models_{w}\square p\to p$, then $\not\models_{w}\square p$, which means there is a $v$ such that $wRv$ and $\not\models_{v}p$. But since $R$ is transitive and $uRw$, we get $uRv$, implying $v\in S$, contradicting the $R$-maximality of $w$. Therefore, $\not\models_{w}\square p\to p$, or $\not\models_{u}\square(\square p\to p)$. As a result, $\models_{u}\square(\square p\to p)\to\square p$. ∎