Let a Heyting algebra $H$ be given. Suppose $x \in H$.
Prove the following: if $\neg \neg x \cong x$, then $x \vee \neg x \cong \top$.
(To be precise: here $\top$ means the (essentially unique) top element of the lattice, and negation $\neg$ is defined as usual in a Heyting algebra, namely $\neg x $ is $x \Rightarrow \bot$. Here $\bot$ is the bottom element of the lattice, of course again essentially unique.)
I tried everything, nothing seems to work. (NB: I managed to prove the converse; my argument was, however, not directly 'reversable'.)