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 )
per cases ( x = 0 or x <> 0 ) ;
suppose x = 0 ; :: thesis: ex m, n being Integer st
( n <> 0 & x = m / n )
then x = 0 / 1 ;
hence ex m, n being Integer st
( n <> 0 & x = m / n ) ; :: thesis: verum
end;
suppose A2: x <> 0 ; :: thesis: ex m, n being Integer st
( 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 )
hereby :: thesis: x = m / n
assume n = 0 ; :: thesis: contradiction
then n " = 0 ;
hence contradiction by A2, A3; :: thesis: verum
end;
thus x = m / n by A3; :: thesis: verum
end;
end;