let n be Nat; :: thesis: ( ex p being non zero Nat st
( p <> 1 & p |^ 2 divides n ) implies n is square-containing )
given p being non zero Nat such that A1: p <> 1 and
A2: p |^ 2 divides n ; :: thesis: n is square-containing
consider r being Prime such that
A3: r divides p by A1, Lm2;
r |^ 2 divides p |^ 2 by A3, WSIERP_1:14;
then r |^ 2 divides n by A2, NAT_D:4;
hence n is square-containing ; :: thesis: verum