theorem lemmod: :: NUMBER01:2

for i, n being Real holds
( not |.i.| = n or i = n or i = - n )