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!