let x be Point of I[01] ; :: thesis: [x,1] in IBB
A1: ( 0 is Point of I[01] & 1 is Point of I[01] ) by BORSUK_1:86;
A2: ( x <= 1 & x >= 0 ) by BORSUK_1:86;
then 2 * x <= 2 * 1 by XREAL_1:66;
then A3: (2 * x) - 1 <= (2 * 1) - 1 by XREAL_1:15;
2 * x >= 2 * 0 by A2;
then 1 - (2 * x) <= 1 - (2 * 0 ) by XREAL_1:15;
hence [x,1] in IBB by A1, A3, Def11; :: thesis: verum