English
Let X be a linearly ordered set endowed with the order topology. Then X is a T5 space (completely normal).
Русский
Пусть X — линейно упорядоченное множество, оснащённое порядковой топологией. Тогда X является T5-пространством (полностью нормальным).
LaTeX
$$$\forall X\left(\mathrm{LinearOrder}(X) \land \mathrm{TopologicalSpace}(X) \land \mathrm{OrderTopology}(X)\right) \Rightarrow \mathrm{T5Space}(X)$$$
Lean4
instance (priority := 100) t5Space : T5Space X :=
T5Space.mk