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 } :: according to XBOOLE_0:def 10 :: thesis: { p where p is Point of [:I[01],I[01]:] : p `2 = (2 * (p `1)) - 1 } c= ICC /\ IBB

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ICC /\ IBB or x in { p where p is Point of [:I[01],I[01]:] : p `2 = (2 * (p `1)) - 1 } )
assume A1: x in ICC /\ IBB ; :: thesis: x in { p where p is Point of [:I[01],I[01]:] : p `2 = (2 * (p `1)) - 1 }
then x in ICC by XBOOLE_0:def 4;
then consider p being Point of [:I[01],I[01]:] such that
A2: x = p and
A3: p `2 <= (2 * (p `1)) - 1 by Th55;
x in IBB by A1, XBOOLE_0:def 4;
then ex q being Point of [:I[01],I[01]:] st
( x = q & q `2 >= 1 - (2 * (q `1)) & q `2 >= (2 * (q `1)) - 1 ) by Th54;
then p `2 = (2 * (p `1)) - 1 by A2, A3, XXREAL_0:1;
hence x in { p where p is Point of [:I[01],I[01]:] : p `2 = (2 * (p `1)) - 1 } by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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 } ; :: thesis: 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; :: thesis: verum