let a, b be Real; ( b - a <= 1 implies for d being set st d in IntIntervals (a,b) holds
CircleMap | d is one-to-one )
assume A1:
b - a <= 1
; for d being set st d in IntIntervals (a,b) holds
CircleMap | d is one-to-one
let d be set ; ( d in IntIntervals (a,b) implies CircleMap | d is one-to-one )
assume
d in IntIntervals (a,b)
; CircleMap | d is one-to-one
then consider n being Element of INT such that
A2:
d = ].(a + n),(b + n).[
;
A3:
CircleMap | [.(a + n),((a + n) + 1).[ is one-to-one
;
(b - a) + (a + n) <= 1 + (a + n)
by A1, XREAL_1:6;
hence
CircleMap | d is one-to-one
by A2, A3, SIN_COS6:2, XXREAL_1:45; verum