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