theorem Th16: :: BORSUK_6:16

{ p where p is Point of (TOP-REAL 2) : p `2 >= (2 * (p `1)) - 1 } is closed Subset of (TOP-REAL 2)