let x be Point of I[01] ; :: thesis: [0 ,x] in IAA
( 0 is Point of I[01] & x <= 1 - (2 * 0 ) ) by BORSUK_1:86;
hence [0 ,x] in IAA by Def10; :: thesis: verum