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