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