set GG = [:I[01] ,I[01] :];
let x be Point of [:I[01] ,I[01] :]; :: thesis: ( x in IAA implies x `1 <= 1 / 2 )
assume x in IAA ; :: thesis: x `1 <= 1 / 2
then consider a, b being Point of I[01] such that
A1: x = [a,b] and
A2: b <= 1 - (2 * a) by Def10;
b >= 0 by BORSUK_1:86;
then 1 >= 0 + (2 * a) by A2, XREAL_1:21;
then A3: 1 / 2 >= (2 * a) / 2 by XREAL_1:74;
x = [(x `1 ),(x `2 )] by A1, MCART_1:8;
hence x `1 <= 1 / 2 by A1, A3, ZFMISC_1:33; :: thesis: verum