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