A1: ( 1 >= 1 - (2 * 0) & 1 >= (2 * 0) - 1 ) ;
( 0 is Point of I[01] & 1 is Point of I[01] ) by BORSUK_1:43;
hence [0,1] in IBB by A1, Def9; :: thesis: verum