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