theorem Th11: :: RING_3:11

for m being Nat
for i being Integer st 0 < m & m * i divides m & not i = 1 holds
i = - 1