theorem Th58: :: BORSUK_6:58

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