theorem Th53: :: BORSUK_6:53

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