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

proof

let x be set ; :: 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 Th67;
A3: x in ICC by A1, XBOOLE_0:def 4;
then y `1 >= 1 / 2 by Th68;
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 5;
A6: y `2 is Point of I[01] by Th31;
ex q being Point of [:I[01] ,I[01] :] st
( q = y & q `2 <= (2 * (q `1 )) - 1 ) by A3, Th63;
then y `2 = 0 by A4, A6, BORSUK_1:86;
then y = [(1 / 2),0 ] by A5, A4, MCART_1:23;
hence x in {[(1 / 2),0 ]} by TARSKI:def 1; :: thesis: verum

end;

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