三角形外角不等式

依赖：对顶角相等、SAS 全等判定、尺子公理、量角器公理。 这是 Euclid I.16，不依赖平行公理——属于"中性几何"结论。

陈述

设 $\triangle ABC$ 非退化。把边 $BC$ 沿 $C$ 延长到点 $D$，得到 $C$ 处的外角 $\angle ACD$。则任一外角严格大于任一不相邻内角：

注意是严格不等式——加上平行公理后才能升级为等式 $\angle ACD = \angle BAC + \angle ABC$（外角等于两个不相邻内角之和），那是 L3 的事。