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