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 Def8;
b >= 0 by BORSUK_1:43;
then 1 >= 0 + (2 * a) by A2, XREAL_1:19;
then A3: 1 / 2 >= (2 * a) / 2 by XREAL_1:72;
thus x `1 <= 1 / 2 by A1, A3; :: thesis: verum