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