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] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) by Def11;
A2: b <= 1 by BORSUK_1:86;
( a = 0 & b = s ) by A1, ZFMISC_1:33;
hence s = 1 by A1, A2, XXREAL_0:1; :: thesis: verum