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 ) }
XBOOLE_0:def 10 { p where p is Point of [:I[01],I[01]:] : ( p `2 >= 1 - (2 * (p `1)) & p `2 >= (2 * (p `1)) - 1 ) } c= IBB
let x be object ; TARSKI:def 3 ( 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 ) }
; 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 2;
then A6:
x = [(x `1),(x `2)]
by MCART_1:21;
( p `1 is Point of I[01] & p `2 is Point of I[01] )
by Th27;
hence
x in IBB
by A4, A5, A6, Def9; verum