theorem Th2: :: KOLMOG01:2

for r being Real holds
( not r * r = r or r = 0 or r = 1 )