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 A2:
(
x in IAA &
x in ICC )
by XBOOLE_0:def 4;
reconsider y =
x as
Point of
[:I[01] ,I[01] :] by A1;
y in the
carrier of
[:I[01] ,I[01] :]
;
then A3:
y in [:the carrier of I[01] ,the carrier of I[01] :]
by BORSUK_1:def 5;
A4:
y `1 >= 1
/ 2
by A2, Th68;
y `1 <= 1
/ 2
by A2, Th67;
then A5:
y `1 = 1
/ 2
by A4, XXREAL_0:1;
consider q being
Point of
[:I[01] ,I[01] :] such that A6:
(
q = y &
q `2 <= (2 * (q `1 )) - 1 )
by A2, Th63;
y `2 is
Point of
I[01]
by Th31;
then
y `2 = 0
by A5, A6, BORSUK_1:86;
then
y = [(1 / 2),0 ]
by A3, A5, MCART_1:23;
hence
x in {[(1 / 2),0 ]}
by TARSKI:def 1;
:: thesis: verum
end;
A7:
1 / 2 is Point of I[01]
by BORSUK_1:86;
then A8:
[(1 / 2),0 ] in IAA
by Th78;
[(1 / 2),0 ] in ICC
by A7, Th77;
then
[(1 / 2),0 ] in IAA /\ ICC
by A8, XBOOLE_0:def 4;
hence
{[(1 / 2),0 ]} c= IAA /\ ICC
by ZFMISC_1:37; :: thesis: verum