let a, b be Real; :: thesis: ( b - a <= 1 implies IntIntervals (a,b) is mutually-disjoint )

assume A1: b - a <= 1 ; :: thesis: IntIntervals (a,b) is mutually-disjoint

assume x in IntIntervals (a,b) ; :: thesis: ( not y in IntIntervals (a,b) or x = y or x misses y )

then consider nx being Element of INT such that

A4: x = ].(a + nx),(b + nx).[ ;

assume y in IntIntervals (a,b) ; :: thesis: ( x = y or x misses y )

then consider ny being Element of INT such that

A5: y = ].(a + ny),(b + ny).[ ;

assume A6: x <> y ; :: thesis: x misses y

assume x meets y ; :: thesis: contradiction

then consider z being object such that

A7: z in x and

A8: z in y by XBOOLE_0:3;

reconsider z = z as Real by A4, A7;

A9: a + nx < z by A4, A7, XXREAL_1:4;

A10: z < b + ny by A5, A8, XXREAL_1:4;

A11: a + ny < z by A5, A8, XXREAL_1:4;

A12: z < b + nx by A4, A7, XXREAL_1:4;

assume A1: b - a <= 1 ; :: thesis: IntIntervals (a,b) is mutually-disjoint

A2: now :: thesis: for k being Element of NAT holds a + (k + 1) >= b

let x, y be set ; :: according to TAXONOM2:def 5 :: thesis: ( not x in IntIntervals (a,b) or not y in IntIntervals (a,b) or x = y or x misses y )let k be Element of NAT ; :: thesis: a + (k + 1) >= b

A3: (a + 1) + 0 <= (a + 1) + k by XREAL_1:6;

(b - a) + a <= 1 + a by A1, XREAL_1:6;

hence a + (k + 1) >= b by A3, XXREAL_0:2; :: thesis: verum

end;A3: (a + 1) + 0 <= (a + 1) + k by XREAL_1:6;

(b - a) + a <= 1 + a by A1, XREAL_1:6;

hence a + (k + 1) >= b by A3, XXREAL_0:2; :: thesis: verum

assume x in IntIntervals (a,b) ; :: thesis: ( not y in IntIntervals (a,b) or x = y or x misses y )

then consider nx being Element of INT such that

A4: x = ].(a + nx),(b + nx).[ ;

assume y in IntIntervals (a,b) ; :: thesis: ( x = y or x misses y )

then consider ny being Element of INT such that

A5: y = ].(a + ny),(b + ny).[ ;

assume A6: x <> y ; :: thesis: x misses y

assume x meets y ; :: thesis: contradiction

then consider z being object such that

A7: z in x and

A8: z in y by XBOOLE_0:3;

reconsider z = z as Real by A4, A7;

A9: a + nx < z by A4, A7, XXREAL_1:4;

A10: z < b + ny by A5, A8, XXREAL_1:4;

A11: a + ny < z by A5, A8, XXREAL_1:4;

A12: z < b + nx by A4, A7, XXREAL_1:4;

per cases
( nx = ny or nx < ny or nx > ny )
by XXREAL_0:1;

end;

suppose
nx < ny
; :: thesis: contradiction

then
nx + 1 <= ny
by INT_1:7;

then reconsider k = ny - (nx + 1) as Element of NAT by INT_1:5;

((a + nx) + 1) + k < b + nx by A12, A11, XXREAL_0:2;

then ((a + nx) + (k + 1)) - nx < (b + nx) - nx by XREAL_1:14;

then a + (k + 1) < b ;

hence contradiction by A2; :: thesis: verum

end;then reconsider k = ny - (nx + 1) as Element of NAT by INT_1:5;

((a + nx) + 1) + k < b + nx by A12, A11, XXREAL_0:2;

then ((a + nx) + (k + 1)) - nx < (b + nx) - nx by XREAL_1:14;

then a + (k + 1) < b ;

hence contradiction by A2; :: thesis: verum

suppose
nx > ny
; :: thesis: contradiction

then
ny + 1 <= nx
by INT_1:7;

then reconsider k = nx - (ny + 1) as Element of NAT by INT_1:5;

((a + ny) + 1) + k < b + ny by A9, A10, XXREAL_0:2;

then ((a + ny) + (k + 1)) - ny < (b + ny) - ny by XREAL_1:14;

then a + (k + 1) < b ;

hence contradiction by A2; :: thesis: verum

end;then reconsider k = nx - (ny + 1) as Element of NAT by INT_1:5;

((a + ny) + 1) + k < b + ny by A9, A10, XXREAL_0:2;

then ((a + ny) + (k + 1)) - ny < (b + ny) - ny by XREAL_1:14;

then a + (k + 1) < b ;

hence contradiction by A2; :: thesis: verum