( { p7 where p7 is Point of (TOP-REAL 2) : - (p7 `1) <= p7 `2 } is closed Subset of (TOP-REAL 2) & { p7 where p7 is Point of (TOP-REAL 2) : p7 `2 <= - (p7 `1) } is closed Subset of (TOP-REAL 2) ) by Lm11, Lm14;