Finite directed set has a greatest element
ID: 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.
New to topics? Read the docs here!