theorem Th18: :: BORSUK_6:18

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