set P = { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 } ;
thus ICC 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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ICC or x in { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 } )
assume A1: x in ICC ; :: thesis: x in { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 }
then consider a, b being Point of I[01] such that
A2: ( x = [a,b] & b <= (2 * a) - 1 ) by Def12;
reconsider x' = x as Point of [:I[01] ,I[01] :] by A1;
( x' `1 = a & x' `2 = b ) by A2, MCART_1:7;
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 )
assume x in { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 } ; :: thesis: x in ICC
then consider p being Point of [:I[01] ,I[01] :] such that
A3: ( p = x & p `2 <= (2 * (p `1 )) - 1 ) ;
x in the carrier of [:I[01] ,I[01] :] by A3;
then x in [:the carrier of I[01] ,the carrier of I[01] :] by BORSUK_1:def 5;
then A4: x = [(x `1 ),(x `2 )] by MCART_1:23;
A5: p `1 is Point of I[01] by Th31;
p `2 is Point of I[01] by Th31;
hence x in ICC by A3, A4, A5, Def12; :: thesis: verum