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:43;
hence [0,x] in IAA by Def8; :: thesis: verum