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: for every compact group $\Sigma'$ and every continuous morphism $\alpha':G\to\Sigma'$, there exists a unique continuous morphism $\beta:\Sigma\to\Sigma'$ such that $\alpha'= \beta\circ\alpha$. 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). Of course, this is not the only way — contrast an epigraph in Reed & Simon, Functional Analysis: “A good definition should be the hypothesis of a theorem. (J. Glimm)”
Added: I took the above example (constructed object) as perhaps the closest to yours. In fact, I should have gone to Dixmier’s relative Bourbaki for it exactly (Algebra I.2.4 “Monoid of fractions”, I.8.12 “Rings of fractions”, I.9.4 “The field of rational numbers”):
Theorem 4. (...)
Definition 8. The ring defined in Theorem 4 is called the ring of fractions (...)