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