theorem Th12: :: BORSUK_6:12

for S, T being Subset of (TOP-REAL 2) st S = { p where p is Point of (TOP-REAL 2) : p `2 >= 1 - (2 * (p `1)) } & T = { p where p is Point of (TOP-REAL 2) : p `2 >= - (p `1) } holds
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S = T