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