thus IAA /\ ICC c= {[(1 / 2),0]} :: according to XBOOLE_0:def 10 :: thesis: {[(1 / 2),0]} c= IAA /\ ICC

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in IAA /\ ICC or x in {[(1 / 2),0]} )
assume A1: x in IAA /\ ICC ; :: thesis: x in {[(1 / 2),0]}
then reconsider y = x as Point of [:I[01],I[01]:] ;
x in IAA by A1, XBOOLE_0:def 4;
then A2: y `1 <= 1 / 2 by Th59;
A3: x in ICC by A1, XBOOLE_0:def 4;
then y `1 >= 1 / 2 by Th60;
then A4: y `1 = 1 / 2 by A2, XXREAL_0:1;
y in the carrier of [:I[01],I[01]:] ;
then A5: y in [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
A6: y `2 is Point of I[01] by Th27;
ex q being Point of [:I[01],I[01]:] st
( q = y & q `2 <= (2 * (q `1)) - 1 ) by A3, Th55;
then y `2 = 0 by A4, A6, BORSUK_1:43;
then y = [(1 / 2),0] by A5, A4, MCART_1:21;
hence x in {[(1 / 2),0]} by TARSKI:def 1; :: thesis: verum

end;

1 / 2 is Point of I[01] by BORSUK_1:43;
then ( [(1 / 2),0] in IAA & [(1 / 2),0] in ICC ) by Th69, Th70;
then [(1 / 2),0] in IAA /\ ICC by XBOOLE_0:def 4;
hence {[(1 / 2),0]} c= IAA /\ ICC by ZFMISC_1:31; :: thesis: verum