let a, b be Real; :: thesis: ( 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 ; :: thesis: for d being set st d in IntIntervals (a,b) holds

CircleMap | d is one-to-one

let d be set ; :: thesis: ( d in IntIntervals (a,b) implies CircleMap | d is one-to-one )

assume d in IntIntervals (a,b) ; :: thesis: 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; :: thesis: verum

CircleMap | d is one-to-one )

assume A1: b - a <= 1 ; :: thesis: for d being set st d in IntIntervals (a,b) holds

CircleMap | d is one-to-one

let d be set ; :: thesis: ( d in IntIntervals (a,b) implies CircleMap | d is one-to-one )

assume d in IntIntervals (a,b) ; :: thesis: 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; :: thesis: verum