let a be Nat; :: thesis: for p being Prime st p |^ 2 divides a holds
p divides a
let p be Prime; :: thesis: ( p |^ 2 divides a implies p divides a )
assume p |^ 2 divides a ; :: thesis: p divides a
then consider t being Nat such that
A1: a = (p |^ 2) * t by NAT_D:def 3;
a = (p * p) * t by A1, WSIERP_1:1
.= p * (p * t) ;
hence p divides a by NAT_D:def 3; :: thesis: verum