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