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