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