Post #1816220

@de_Jong_Tom @dwarn Cool. In particular, people sometimes define lattices in terms of their partial order, and sometimes in terms of their algebraic operations. So it's useful to know that we can prove they're discrete either way.