for m, n being Nat st m * n is square-free holds
m is square-free by NAT_D:9;