consider m, n being Integer such that
n > 0 and
A1: p = m / n by Th2;
- p = (- m) / n by A1;
hence - p is rational ; :: thesis: verum