  Maria Pia Sol\`er has recently proved that an orthomodular form that has an
infinite orthonormal sequence is real, complex, or quaternionic Hilbert space.
This paper provides an exposition of her result, and describes its consequences
for Baer $\ast$-rings, infinite-dimensional projective geometries, orthomodular
lattices, and Mackey's quantum logic.
