Finite directed set has a greatest element
= Finite directed set has a greatest element
In a finite nonempty <directed set>, repeatedly take an internal common <upper bound> of the element reached so far and the next element. The final member is above every element of the <directed set> and is therefore its <greatest element> and <least upper bound>.