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 x in ICC /\ IBB ; :: thesis: x in { p where p is Point of [:I[01] ,I[01] :] : p `2 = (2 * (p `1 )) - 1 }
then A1: ( x in ICC & x in IBB ) by XBOOLE_0:def 4;
then consider p being Point of [:I[01] ,I[01] :] such that
A2: ( x = p & p `2 <= (2 * (p `1 )) - 1 ) by Th63;
consider q being Point of [:I[01] ,I[01] :] such that
A3: ( x = q & q `2 >= 1 - (2 * (q `1 )) & q `2 >= (2 * (q `1 )) - 1 ) by A1, Th62;
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 & p `2 = (2 * (p `1 )) - 1 ) ;
x in the carrier of [:I[01] ,I[01] :] by A4;
then A5: x in [:the carrier of I[01] ,the carrier of I[01] :] by BORSUK_1:def 5;
then A6: x = [(p `1 ),(p `2 )] by A4, MCART_1:23;
A7: ( p `1 in the carrier of I[01] & p `2 in the carrier of I[01] ) by A4, A5, MCART_1:10;
then A8: x in ICC by A4, A6, Def12;
(2 * (p `1 )) - 1 >= 0 by A4, A7, 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 A4, A6, A7, Def11;
hence x in ICC /\ IBB by A8, XBOOLE_0:def 4; :: thesis: verum