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

proof

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