let p be prime Nat; :: thesis: for k being square Nat st p divides k holds
p ^2 divides k
let k be square Nat; :: thesis: ( p divides k implies p ^2 divides k )
consider a being Nat such that
A1: a ^2 = k by PYTHTRIP:def 3;
assume p divides k ; :: thesis: p ^2 divides k
hence p ^2 divides k by A1, NAT_3:5, NEWTON02:15; :: thesis: verum