assume 1 is square-containing ; :: thesis: contradiction
then consider n being Prime such that
A1: n |^ 2 divides 1 ;
n * n divides 1 by A1, WSIERP_1:1;
then ( n = 1 or n = - 1 ) by WSIERP_1:15, XCMPLX_1:182;
hence contradiction by INT_2:def 4; :: thesis: verum