Description: The join of a poset commutes. (The antecedent
<. X , Y >. e. dom .\/ /\ <. Y , X >. e. dom .\/ i.e. "the joins
exist" could be omitted as an artifact of our particular join
definition, but other definitions may require it.) (Contributed by NM, 16-Sep-2011)(Revised by NM, 12-Sep-2018)