theorem Th55: :: BORSUK_6:55

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