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