theorem Th2: :: NIVEN:2

for a, b being Real holds
( not |.a.| = b or a = b or a = - b )