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