theorem Th17: :: BORSUK_6:17

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