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 set ; :: 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 Th63;
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 Th62;
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 set ; :: 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 5;
then A7: ( x = [(p `1 ),(p `2 )] & p `1 in the carrier of I[01] ) by A4, MCART_1:10, MCART_1:23;
A8: p `2 in the carrier of I[01] by A4, A6, MCART_1:10;
then A9: x in ICC by A5, A7, Def12;
(2 * (p `1 )) - 1 >= 0 by A5, A8, BORSUK_1:86;
then 2 * (p `1 ) >= 0 + 1 by XREAL_1:21;
then (2 * (p `1 )) / 2 >= 1 / 2 by XREAL_1:74;
then ( (2 * (p `1 )) - 1 >= 0 & 0 >= 1 - (2 * (p `1 )) ) by XREAL_1:221, XREAL_1:222;
then x in IBB by A5, A7, A8, Def11;
hence x in ICC /\ IBB by A9, XBOOLE_0:def 4; :: thesis: verum