let x be object ; :: thesis: ( x in RAT implies ex m, n being Integer st

( n <> 0 & x = m / n ) )

assume A1: x in RAT ; :: thesis: ex m, n being Integer st

( n <> 0 & x = m / n )

( n <> 0 & x = m / n ) )

assume A1: x in RAT ; :: thesis: ex m, n being Integer st

( n <> 0 & x = m / n )

per cases
( x = 0 or x <> 0 )
;

end;

suppose A2:
x <> 0
; :: thesis: ex m, n being Integer st

( n <> 0 & x = m / n )

( n <> 0 & x = m / n )

consider m, n being Integer such that

A3: x = m / n by A1, Def1;

take m ; :: thesis: ex n being Integer st

( n <> 0 & x = m / n )

take n ; :: thesis: ( n <> 0 & x = m / n )

end;A3: x = m / n by A1, Def1;

take m ; :: thesis: ex n being Integer st

( n <> 0 & x = m / n )

take n ; :: thesis: ( n <> 0 & x = m / n )

hereby :: thesis: x = m / n

thus
x = m / n
by A3; :: thesis: verumassume
n = 0
; :: thesis: contradiction

then n " = 0 ;

hence contradiction by A2, A3; :: thesis: verum

end;then n " = 0 ;

hence contradiction by A2, A3; :: thesis: verum