theorem Th22: :: BORSUK_6:22

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