let s be set ; ( [s,1] in ICC implies s = 1 )
assume
[s,1] in ICC
; 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; verum