theorem Th13: :: JGRAPH_2:13

for p being Point of (TOP-REAL 2) holds
( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) )