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