Applying perp twice in a hilbert space

Question

Let $H$ be a hilbert space and let $K \subset H$ be a subspace. Then $\overline{K} \subset K^{\perp\perp}$, but why does the reverse inclusion hold?

Answer 1

If $x\not\in\overline K$, then there exists $x_1=x+k\in x+\overline K$ with $x_1\neq 0$ and $x_1\bot K$ (take $x_1=x-Px$, where $P$ denotes the othogonal projection onto $\overline K$). If $x$ were an element of $K^{\bot\bot}$, then, in particular we would have $x\bot x_1$. But $\langle x,x_1\rangle =\langle x_1,x_1\rangle >0$. Hence, $x\not\in K^{\bot\bot}$.