assume A1: q ^2 is integer ; :: thesis: contradiction
consider m, n being Integer such that
A2: n > 0 and
A3: q = m / n by RAT_1:2;
q ^2 = (m ^2) / (n ^2) by A3, XCMPLX_1:76;
then n divides m by A1, A2, Th4, POLYNOM9:3;
then m mod n = 0 by A2, INT_1:62;
then m / n = m div n by PEPIN:63;
hence contradiction by A3; :: thesis: verum