English
In a directed partially ordered set, no element can be both minimal and maximal.
Русский
В направленном частично упорядоченном множестве не существует элемента, который одновременно был бы минимальным и максимальным.
LaTeX
$$$\forall \{\beta\}, [\text{PartialOrder }\beta], [\text{Nontrivial }\beta], [\text{IsDirected }\beta (\le )], \forall b:\beta, \ IsMin(b) \rightarrow \neg IsMax(b).$$$
Lean4
protected theorem not_isMax' [IsDirected β (· ≤ ·)] {b : β} (hb : IsMin b) : ¬IsMax b := fun hb' ↦
hb'.toDual.not_isMax hb.toDual