set GG = [:I[01] ,I[01] :];
let x be Point of [:I[01] ,I[01] :]; :: thesis: ( x in ICC implies x `1 >= 1 / 2 )
assume x in ICC ; :: thesis: x `1 >= 1 / 2
then consider a, b being Point of I[01] such that
A1: ( x = [a,b] & b <= (2 * a) - 1 ) by Def12;
b >= 0 by BORSUK_1:86;
then 0 + 1 <= 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