:: deftheorem defines CircleMap TOPREALB:def 12 :
for r being Point of R^1 holds CircleMap r = CircleMap | ].r,(r + 1).[;