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;