let m, n be natural number ; :: thesis: ( not m is square-containing & n divides m implies not n is square-containing )
assume A1: ( not m is square-containing & n divides m ) ; :: thesis: not n is square-containing
then ex x being Nat st m = n * x by NAT_D:def 3;
hence not n is square-containing by A1, Th25; :: thesis: verum