Dixmier always solves this as follows, e.g. in *C\*-algebras* — surely one possible example of good exposition (E. C. Lance’s translator‘s preface: “With is clear and straightforward style, this remains the best book form which to learn about *C\**-algebras”): >**16.1. The compact group associated with a topological group** >**16.1.1. Theorem.** *Let $G$ be a topological group. There exists a compact group $\Sigma$ and a continuous morphism $\alpha:G\to\Sigma$ possessing the following property:* (...). *Furthermore, the pair $(\Sigma,\alpha)$ is determined up to isomorphism by this property.* >(... Long proof goes here ...) >**16.1.2. Definition.** The group $\Sigma$ is called the *compact group associated with* $G$, and $\alpha$ is called the *canonical morphism of $G$ into $\Sigma$*. The book has about two dozen “X.Y.2” definitions like this — e.g. no less than six over pp. 116–123 (disjoint representations, factor representation, quasi-equivalent representations, type I, multiplicity-free, multiplicity), and the almost last statement in the book is a definition (Plancherel measure). ---- **Added:** I took the above example as perhaps the closest to yours (constructed object). In fact Dixmier’s relative Bourbaki does yours *exactly*, just the same down to the use of a subtitle (Algebra I.2.4 “Monoid of fractions”, I.8.12 [“Rings of fractions”](https://archive.org/details/ElementsOfMathematics-AlgebraPart1/page/n136), I.9.4 “The field of rational numbers”): > **12. Rings of fractions** > **Theorem 4.** (...) > **Definition 8.** *The ring defined in Theorem* 4 *is called the ring of fractions* (...) Of course, this “classic” way is not the only one: I also agree with Nik Weaver’s answer, and with this contrasting epigraph in Reed & Simon, *Functional Analysis* (my emphasis): “A good definition should be the ***hypothesis*** of a theorem. (J. Glimm)”