let x be set ; :: thesis: ( ex m, n being Integer st x = m / n implies x is rational )
( x is Rational iff x in RAT ) by Def2;
hence ( ex m, n being Integer st x = m / n implies x is rational ) by Def1; :: thesis: verum