theorem Th54: :: BORSUK_6:54

IBB = { p where p is Point of [:I[01],I[01]:] : ( p `2 >= 1 - (2 * (p `1)) & p `2 >= (2 * (p `1)) - 1 ) }