let r be Real; :: thesis: ( frac r = 1 / 2 implies CircleMap . r = |[(- 1),0]| )
assume A1: frac r = 1 / 2 ; :: thesis: CircleMap . r = |[(- 1),0]|
thus CircleMap . r = CircleMap . (r + (- [\r/])) by Th31
.= CircleMap . (r - [\r/])
.= |[(- 1),0]| by A1, Lm19, INT_1:def 8 ; :: thesis: verum