mixing theorem with definition (definition with proof) I often find myself writing a definition which requires a proof. You are defining a term and, contextually, need to prove that the definition makes sense. 
How can you express that? What about a definition with a proof?
Sometime one can write the definition and then the theorem. But often happens that many definition which should stay together need to be split 
because a theorem is required in between.
A tentative example:
Definition (rational numbers)
Let $\sim$ be the equivalence relation on $\mathbb Z^*\times \mathbb Z$ given 
by
$$
  (q,p) \sim (q',p') \iff pq' = p'q.
$$
We define $\mathbb Q= (\mathbb Z^*\times \mathbb Z)/\sim$. 
On $\mathbb Q$ we define addition and multiplication as follows 
$$
   [(q,p)] + [(q',p')] = [(qq',pq'+p'q)] \\
   [(q,p)] \cdot[(q',p')] = [(qq',pp')]
$$
With these operations and choosing 
$0_\mathbb Q=[(1,0)]$, and $1_\mathbb Q=[(1,1)]$ 
turns out that $\mathbb Q$ is a field.
Proof.
We are going to prove that $\sim$ is indeed an equivalence relation,
that addition and multiplication are well defined and that the resulting 
set is a field. [...]
 A: 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 from 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”, 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)”
A: $\newcommand{\Z}{\mathbb{Z}}
\newcommand{\Q}{\mathbb{Q}}$
I think the notion of "well-defined" may not always be well defined and should perhaps be avoided. In your example, it may be unclear what exactly is being proved. 
I also think it is all right to introduce notions within a statement; this can be done without ambiguity by using terms such as "define" and "introduce" and/or the symbol "$:=$" meaning "[is] defined as". I have done it many times in my papers and never had a reviewer complain about that. In particular, your example could be rewritten as follows. 

\subsection{Rational numbers}
The following proposition introduces, in a justified manner, the field of rational numbers.  

Proposition 
(I) The binary relation $\sim$ on $P:=\Z\times\Z^*$ defined by the condition 
  \begin{equation}
(p_1,q_1)\sim(p_2,q_2)\iff p_1q_2=p_2q_1 
\end{equation}
  for $(p_1,q_1)$ and $(p_2,q_2)$ in $P$ is an equivalence. Let then 
  \begin{equation}
 \Q:=P/\sim. 
\end{equation}
(II) Consider the binary operations $\oplus$ and $\odot$ on $P$ defined by the formulas 
  \begin{align}
 (p_1,q_1)\oplus(p_2,q_2)&:=(p_1q_2+p_2q_1,q_1q_2), \\ 
 (p_1,q_1)\odot(p_2,q_2)&:=(p_1p_2,q_1q_2) 
\end{align}
  for $(p_1,q_1)$ and $(p_2,q_2)$ in $P$. Then for any $r_1,\tilde r_1,r_2,\tilde r_2$ in $P$ such that $r_1\sim\tilde r_1$ and $r_2\sim\tilde r_2$ we have 
  \begin{equation}
 r_1\oplus r_2\sim\tilde r_1\oplus\tilde r_2\quad\text{and}\quad r_1\odot r_2\sim\tilde r_1\odot\tilde r_2. 
\end{equation}
(III) 
  Define now the binary operations $+$ and $\cdot$ on $\Q$ by the formulas
\begin{equation}
 [r_1]+[r_2]:=[r_1\oplus r_2]\quad\text{and}\quad [r_1]\cdot[r_2]:=[r_1\odot r_2] 
\end{equation}
  for all $r_1,r_2$ in $P$. 
  Let also $0_\Q:=[(0,1)]$ and $1_\Q:=[(1,1)]$. Then $(\Q,+,\cdot,0_\Q,1_\Q)$ is a field. 

Proof. $\ldots$ 

A: One approach always available is to decompose your problem into a series of definitions and theorems each of which is formally correct and relies only on the previous ones. It may require defining and naming sub-objects. For example: (1) Definition of ~. (2) Theorem: ~ is an equivalence relation. Proof. (3) Definition of the set Q. (4) Definition of the + operation. (5) Definition of the x operation. (6) Theorem: (Q,+,x) is a field. Proof.[0]
This decomposition must be possible, otherwise what you are trying to do is not formally correct. But I admit, it feels inelegant. We are taking up more space and time than we "need". We are introducing apparently "global" definitions ~,+,x but we know these are really "local" to the definition of the field Q.
So I think one just has to decide stylistically whether it sacrifices clarity to compress this into a single more concise definition. This is harder if you are introducing a new definition nobody has seen before. In this case you can consider wrapping the whole construction into a subsection of the paper with a summary/overview. ("The goal of this part is to define Q, but to do so we need some intermediate objects...").

[0] A similar common example is to define a function $f: A \to B$ in some way and prove it is well-defined. Formally this can be broken into two steps, e.g. (1) define the relation $f$, (2) Theorem: $f$ is a function. In both cases you want to define a _____, but really you are first defining an object then proving it is a _____.
A: I disagree with the implication that it's always necessary, when trying to write something to be understood, that every sentence has to be a logical consequence of previous sentences or assumed background knowledge.
If you're careful about it, and you say this is what you're doing, I think it can be pedagogical to state a definition first and then show that it makes sense. Especially if the verification is routine and you don't want the definition to be buried among a mass of trivialities. I can give examples of this from my own writing.
