Traditionally, to prove the associativity of the least upper bounds, i.e. we need few lines to prove the inequality from the left hand side and conversely. However, by turning the definition of finit join to the adjunction form, we have a more compact and algebraic-like way to do it.
Let be a poset and be the Cartesian product with Cartesian order which is induced by the product diagram. Note if and only if where . Therefore . Finally, for every implies .
We can also prove some properties automatically from this form. To see , just replace with ; to see replace with itself.