].(a + 0),(b + 0).[ in IntIntervals (a,b) by Lm1;
hence not IntIntervals (a,b) is empty ; :: thesis: verum