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