theorem Th20: :: TOPALG_5:20

for r being Real holds cLoop r = CircleMap * (ExtendInt r)