theorem Th21: :: BORSUK_6:21

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