let x be Point of I[01]; :: thesis: ( x >= 1 / 2 implies [x,0] in ICC )
assume x >= 1 / 2 ; :: thesis: [x,0] in ICC
then 2 * x >= 2 * (1 / 2) by XREAL_1:64;
then A1: (2 * x) - 1 >= (2 * (1 / 2)) - 1 by XREAL_1:13;
0 is Point of I[01] by BORSUK_1:43;
hence [x,0] in ICC by A1, Def10; :: thesis: verum