theorem Th26: :: BORSUK_6:26

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