角平分线 ⟹ 到两边等距（逆命题延后到 `hl-congruence`）

依赖：SAS 全等判定。 当前层只证正向：逆命题（到两边等距 ⟹ 在角平分线上）将延后到 HL 全等判定（直角三角形） 之后给出。

陈述

已知：$OM$ 是 $\angle AOB$ 的角平分线（即 $\angle AOM = \angle MOB$）。$P$ 是 $OM$ 上异于 $O$ 的一点，过 $P$ 分别向 $OA$、$OB$ 作垂线，垂足为 $E$、$F$。

求证：

本节只证此正向（在角平分线上 $\Rightarrow$ 到两边等距）。逆向（到两边等距 $\Rightarrow$ 在角平分线上）延后到 HL 全等判定（直角三角形） 之后给出，见 关于逆命题。