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

( 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