let b, a be real number ; :: thesis: ( b - a <= 1 implies IntIntervals a,b is mutually-disjoint )
assume A1: b - a <= 1 ; :: thesis: IntIntervals a,b is mutually-disjoint
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 )
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
A2: 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
A3: y = ].(a + ny),(b + ny).[ ;
assume A4: x <> y ; :: thesis: x misses y
assume x meets y ; :: thesis: contradiction
then consider z being set such that
A5: z in x and
A6: z in y by XBOOLE_0:3;
reconsider z = z as Real by A2, A5;
A7: ( a + nx < z & z < b + nx ) by A2, A5, XXREAL_1:4;
A8: ( a + ny < z & z < b + ny ) by A3, A6, XXREAL_1:4;

A9: now

let k be Element of NAT ; :: thesis: a + (k + 1) >= b
A10: (b - a) + a <= 1 + a by A1, XREAL_1:8;
(a + 1) + 0 <= (a + 1) + k by XREAL_1:8;
hence a + (k + 1) >= b by A10, XXREAL_0:2; :: thesis: verum

end;

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

suppose nx = ny ; :: thesis: contradiction

hence contradiction by A2, A3, A4; :: thesis: verum

end;

suppose nx < ny ; :: thesis: contradiction

then nx + 1 <= ny by INT_1:20;
then reconsider k = ny - (nx + 1) as Element of NAT by INT_1:18;
((a + nx) + 1) + k < b + nx by A7, A8, XXREAL_0:2;
then ((a + nx) + (k + 1)) - nx < (b + nx) - nx by XREAL_1:16;
then a + (k + 1) < b ;
hence contradiction by A9; :: thesis: verum

end;

suppose nx > ny ; :: thesis: contradiction

then ny + 1 <= nx by INT_1:20;
then reconsider k = nx - (ny + 1) as Element of NAT by INT_1:18;
((a + ny) + 1) + k < b + ny by A7, A8, XXREAL_0:2;
then ((a + ny) + (k + 1)) - ny < (b + ny) - ny by XREAL_1:16;
then a + (k + 1) < b ;
hence contradiction by A9; :: thesis: verum

end;

end;