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] & b <= (2 * a) - 1 ) by Def12;
A2: a <= 1 by BORSUK_1:86;
A3: ( a = s & b = 1 ) by A1, ZFMISC_1:33;
then 1 + 1 <= 2 * a by A1, XREAL_1:21;
then 2 / 2 <= (2 * a) / 2 by XREAL_1:74;
hence s = 1 by A2, A3, XXREAL_0:1; :: thesis: verum