Let $K$ be the modal logic extending classical propositional logic by adding the necessitation rule
N: if $\vdash A$, then $\vdash \square A$
and the distribution axiom
K: $\square(A \rightarrow B) \rightarrow (\square A \rightarrow \square B)$
and let's add moreover the reflexivity axiom
T: $\square A \rightarrow A$
and the axiom
5: $\diamond A \rightarrow \square \diamond A$
How can one then prove the symmetry axiom
B: $A \rightarrow \square \diamond A$
from these?
It seems that some transformations need to be done, but nothing works for me.
$1. \ \square \neg A \rightarrow \neg A$ ;; by T
$2. \ A \rightarrow \neg \square \neg A$ ;; classical tautology (Modus Tollens + $\neg\neg$-elimination) from line $1.$
$3. \ A \rightarrow \diamond A$ ;; definition of $\diamond$ in terms of $\square$, from line $2.$
$4. \ \diamond A \rightarrow \square \diamond A$ ;; by axiom 5
$5. \ A \rightarrow \square \diamond A$ ;; classical tautology (Hypothetical syllogism), from lines $3.$ and $4.$