Holland representation theorem (source code)

= Holland representation theorem
{c}

Every <lattice-ordered group> embeds in a <lattice-ordered permutation group> on one <totally ordered set>. Choose a <value in a lattice-ordered group> for each nonidentity element, act on its ordered right cosets, and combine these chains in an <order sum>. The original element moves its own value's identity coset, making the action faithful. The coset lattice formulas make the embedding preserve both <join> and <meet>.