let m, n be Nat; :: thesis: ( m * n is square-free implies m is square-free )
assume A1: m * n is square-free ; :: thesis: m is square-free
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