It's not part of the definition, but the proof is easy.
Suppose one has a rational number <nobr aria-hidden="true">mn</nobr>[math]\displaystyle{ \lt mfrac\gt \lt mi\gt m\lt /mi\gt \lt mi\gt n\lt /mi\gt \lt /mfrac\gt }[/math]<script type="math/tex" id="MathJax-Element-6">\frac{m}{n}</script> that is reducible. We can assume <nobr aria-hidden="true">n≥1</nobr>[math]\displaystyle{ \lt mi\gt n\lt /mi\gt \lt mo\gt ≥\lt /mo\gt \lt mn\gt 1\lt /mn\gt }[/math]<script type="math/tex" id="MathJax-Element-7">n \ge 1</script> (divide the numerator and denominator by <nobr aria-hidden="true">−1</nobr>[math]\displaystyle{ \lt mo\gt −\lt /mo\gt \lt mn\gt 1\lt /mn\gt }[/math]<script type="math/tex" id="MathJax-Element-8">-1</script> otherwise).
Take an integer <nobr aria-hidden="true">k≥2</nobr>[math]\displaystyle{ \lt mi\gt k\lt /mi\gt \lt mo\gt ≥\lt /mo\gt \lt mn\gt 2\lt /mn\gt }[/math]<script type="math/tex" id="MathJax-Element-9">k \ge 2</script> which divides both of <nobr aria-hidden="true">m</nobr>[math]\displaystyle{ \lt mi\gt m\lt /mi\gt }[/math]<script type="math/tex" id="MathJax-Element-10">m</script> and <nobr aria-hidden="true">n</nobr>[math]\displaystyle{ \lt mi\gt n\lt /mi\gt }[/math]<script type="math/tex" id="MathJax-Element-11">n</script>, and so <nobr aria-hidden="true">m′=m/k</nobr>[math]\displaystyle{ \lt msup\gt \lt mi\gt m\lt /mi\gt \lt mo\gt ′\lt /mo\gt \lt /msup\gt \lt mo\gt =\lt /mo\gt \lt mi\gt m\lt /mi\gt \lt mrow class="MJX-TeXAtom-ORD"\gt \lt mo\gt /\lt /mo\gt \lt /mrow\gt \lt mi\gt k\lt /mi\gt }[/math]<script type="math/tex" id="MathJax-Element-12">m' = m/k</script> and <nobr aria-hidden="true">n′=n/k</nobr>[math]\displaystyle{ \lt msup\gt \lt mi\gt n\lt /mi\gt \lt mo\gt ′\lt /mo\gt \lt /msup\gt \lt mo\gt =\lt /mo\gt \lt mi\gt n\lt /mi\gt \lt mrow class="MJX-TeXAtom-ORD"\gt \lt mo\gt /\lt /mo\gt \lt /mrow\gt \lt mi\gt k\lt /mi\gt }[/math]<script type="math/tex" id="MathJax-Element-13">n'=n/k</script> are smaller integers satisfying <nobr aria-hidden="true">m′n′=mn</nobr>[math]\displaystyle{ \lt mfrac\gt \lt msup\gt \lt mi\gt m\lt /mi\gt \lt mo\gt ′\lt /mo\gt \lt /msup\gt \lt msup\gt \lt mi\gt n\lt /mi\gt \lt mo\gt ′\lt /mo\gt \lt /msup\gt \lt /mfrac\gt \lt mo\gt =\lt /mo\gt \lt mfrac\gt \lt mi\gt m\lt /mi\gt \lt mi\gt n\lt /mi\gt \lt /mfrac\gt }[/math]<script type="math/tex" id="MathJax-Element-14">\frac{m'}{n'} = \frac{m}{n}</script>.
Repeat this process as long as the fraction remains reducible.
One cannot repeat forever, because the sequence of denominators is a sequence of positive integers that gets smaller and smaller, and no such sequence can continue infinitely (essentially one is using mathematical induction in this step).
When the process stops, one has an irreducible fraction representing the same rational number