theorem Th25: :: MOEBIUS1:25

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