Greatest and Least Element

DEF-GR. Greatest and Least Element.

Let $(X,\preceq)$ be a preordered set and $a\in X$.

• $a$ is a greatest element of $X$ if

  \[\forall x\in X : x\preceq a.\]

• $a$ is a least element of $X$ if

  \[\forall x\in X : a\preceq x.\]

PROP-GR-MA.

• Any greatest element is maximal.

• Any least element is minimal.