theorem :: JGRAPH_2:46

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