theorem Th34: :: TOPREALB:34
for r being Real st frac r = 1 / 2 holds
CircleMap . r = |[(- 1),0]|