theorem :: TOPREALB:36
for r being Real st frac r = 3 / 4 holds
CircleMap . r = |[0,(- 1)]|