Let $I$ be an D1128: Inner product space such that

(i)	$\langle \cdot, \cdot \rangle$ is the D34: Inner product in $I$
(ii)	$\perp$ is an D2024: Orthogonality relation on $I$

Let $x, y \in I$ such that $\langle x, y \rangle = 0$. Since $\langle x, y \rangle \in \mathbb{R}$, applying R2413: Complex conjugate of real number and the conjugate symmetry of inner products, we conclude \begin{equation} \langle y, x \rangle = \overline{\langle x, y \rangle} = \langle x, y \rangle = 0 \end{equation} $\square$