let x be set ; :: thesis: ( x is Rational implies ex m, n being Integer st
( n <> 0 & x = m / n ) )
assume x is Rational ; :: thesis: ex m, n being Integer st
( n <> 0 & x = m / n )
then x in RAT by Def2;
hence ex m, n being Integer st
( n <> 0 & x = m / n ) by Th1; :: thesis: verum