Angle bisector test

Dependencies: HL (hypotenuse-leg) congruence, Perpendicular from a point to a line exists and is unique. At this layer we complete the converse of the forward theorem Angle bisector ⇔ equidistant from sides: a point inside $\angle AOB$ that is equidistant from the two sides must lie on the angle bisector.

Statement

Let $\angle AOB$ be a nonzero, non-straight angle, and $P$ a point inside $\angle AOB$ distinct from $O$. Drop perpendiculars from $P$ to $OA$ and $OB$, with feet $M$ and $N$ (i.e. $PM \perp OA$ at $M$ and $PN \perp OB$ at $N$). If

then the ray $OP$ is the Angle bisector ⇔ equidistant from sides of $\angle AOB$, i.e.