let s be set ; :: thesis: ( [s,1] in ICC implies s = 1 )
assume [s,1] in ICC ; :: thesis: s = 1
then consider a, b being Point of I[01] such that
A1: [s,1] = [a,b] and
A2: b <= (2 * a) - 1 by Def10;
b = 1 by A1, XTUPLE_0:1;
then 1 + 1 <= 2 * a by A2, XREAL_1:19;
then A3: 2 / 2 <= (2 * a) / 2 by XREAL_1:72;
( a <= 1 & a = s ) by A1, BORSUK_1:43, XTUPLE_0:1;
hence s = 1 by A3, XXREAL_0:1; :: thesis: verum