Greatest Element of a Finite Family in a Totally Ordered Set

Let $A$ be a set equipped with a \reftext{def:total-order-c54-2026a}{total order} $\le$, let $n$ be a \reftext{def:natural-numbers-2026a}{natural number}, let $[n]$ be the \reftext{def:initial-segment-natural-numbers-2026a}{initial segment} determined by $n$, and let $c\in A^{n}$ be an \reftext{def:finite-tuple-power-2026a}{$n$-tuple} in $A$, with components $c_{k}$.

Then there exists $j\in[n]$ such that $c_{k}\le c_{j}$ for every $k\in[n]$.