Löb axiom implies positive introspection ($\square X\to \square \square X$)

The Löb axiom $\square (\square A\to A)\to \square A$ over normal modal logic already implies $\square X\to \square \square X$. Put $C=\square X\wedge X$. Distribution gives $\square C\to \square X$, hence $X\to (\square C\to C)$. Necessitation and distribution give $\square X\to \square (\square C\to C)$; the Löb axiom gives $\square C$, which implies $\square \square X$.