let m, n be natural number ; :: thesis: ( not m * n is square-containing implies not m is square-containing )
assume A1: not m * n is square-containing ; :: thesis: not m is square-containing
assume m is square-containing ; :: thesis: contradiction
then consider p being Prime such that
A2: p |^ 2 divides m by Def1;
p |^ 2 divides m * n by A2, NAT_D:9;
hence contradiction by A1, Def1; :: thesis: verum