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

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

陈述

角平分线：设 $\angle AOB$ 是一个非零非平角的角。若射线 $OM$ 在 $\angle AOB$ 内部并满足

则称 $OM$ 是 $\angle AOB$ 的角平分线——由公理 III（量角器公理）给出的"半角"实数恰好对应一条这样的射线，存在且唯一。

点到直线的距离：设 $\ell$ 是直线、$P$ 是不在 $\ell$ 上的点。由公理 III，从 $P$ 向 $\ell$ 作垂线，垂足唯一；记之为 $E$。则距离 $\operatorname{dist}(P,\ell) := |PE|$。

完整双向命题——

设 $P$ 是 $\angle AOB$ 内部异于 $O$ 的一点，从 $P$ 分别向 $OA$、$OB$ 作垂线，垂足为 $E$、$F$。则

本节只证 ($\Rightarrow$) 正向：$P$ 在角平分线上 $\Rightarrow |PE|=|PF|$。 逆向 ($\Leftarrow$) 要等到 HL 之后；理由在 关于逆命题 一节。