set KK = { p where p is Point of [:I[01],I[01]:] : p `2 = (2 * (p `1)) - 1 } ;
thus
ICC /\ IBB c= { p where p is Point of [:I[01],I[01]:] : p `2 = (2 * (p `1)) - 1 }
XBOOLE_0:def 10 { p where p is Point of [:I[01],I[01]:] : p `2 = (2 * (p `1)) - 1 } c= ICC /\ IBB
let x be object ; TARSKI:def 3 ( not x in { p where p is Point of [:I[01],I[01]:] : p `2 = (2 * (p `1)) - 1 } or x in ICC /\ IBB )
assume
x in { p where p is Point of [:I[01],I[01]:] : p `2 = (2 * (p `1)) - 1 }
; x in ICC /\ IBB
then consider p being Point of [:I[01],I[01]:] such that
A4:
p = x
and
A5:
p `2 = (2 * (p `1)) - 1
;
x in the carrier of [:I[01],I[01]:]
by A4;
then A6:
x in [: the carrier of I[01], the carrier of I[01]:]
by BORSUK_1:def 2;
then A7:
( x = [(p `1),(p `2)] & p `1 in the carrier of I[01] )
by A4, MCART_1:10, MCART_1:21;
A8:
p `2 in the carrier of I[01]
by A4, A6, MCART_1:10;
then A9:
x in ICC
by A5, A7, Def10;
(2 * (p `1)) - 1 >= 0
by A5, A8, BORSUK_1:43;
then
2 * (p `1) >= 0 + 1
by XREAL_1:19;
then
(2 * (p `1)) / 2 >= 1 / 2
by XREAL_1:72;
then
( (2 * (p `1)) - 1 >= 0 & 0 >= 1 - (2 * (p `1)) )
by XREAL_1:219, XREAL_1:220;
then
x in IBB
by A5, A7, A8, Def9;
hence
x in ICC /\ IBB
by A9, XBOOLE_0:def 4; verum