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
A2: now :: thesis: for k being Element of NAT holds a + (k + 1) >= b
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;
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
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;
suppose nx = ny ; :: thesis: contradiction
hence contradiction by A4, A5, A6; :: thesis: verum
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;
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;
end;