theorem Th23: :: BORSUK_6:23

{ p where p is Point of [:R^1,R^1:] : ( p `2 >= 1 - (2 * (p `1)) & p `2 >= (2 * (p `1)) - 1 ) } is closed Subset of [:R^1,R^1:]