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] & b <= 1 - (2 * a) ) by Def10;
b >= 0 by BORSUK_1:86;
then 1 >= 0 + (2 * a) by A1, XREAL_1:21;
then A2: 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, A2, ZFMISC_1:33; :: thesis: verum