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