English
If α is a bounded order, NonemptyInterval α has a top element, namely the interval [⊥, ⊤], and every interval is below it.
Русский
Если упорядоченность α ограничена сверху и снизу, то у NonemptyInterval α есть верхний элемент, равный интервалу [⊥, ⊤], и каждый интервал лежит ниже него.
LaTeX
$$$\text{top}_{\mathrm{NonemptyInterval}(\alpha)} = [\bot, \top], \quad (\forall s\in \mathrm{NonemptyInterval}(\alpha),\; s \le \top)$$$
Lean4
instance : OrderTop (NonemptyInterval α) where
top := ⟨⟨⊥, ⊤⟩, bot_le⟩
le_top _ := ⟨bot_le, le_top⟩