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