let p be Prime; :: thesis: p is square-free
assume p is square-containing ; :: thesis: contradiction
then consider n being Prime such that
A1: n |^ 2 divides p ;
A2: n divides n |^ 2 by NAT_3:3;
then A3: n divides p by A1, NAT_D:4;

per cases ( n = 1 or n = p ) by A3, INT_2:def 4;

suppose n = 1 ; :: thesis: contradiction

hence contradiction by INT_2:def 4; :: thesis: verum

end;

suppose n = p ; :: thesis: contradiction

then n = n |^ 2 by A1, A2, NAT_D:5;
then n |^ 1 = n |^ 2 ;
then n <= 1 by PEPIN:30;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

end;