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