theorem Th64: :: JGRAPH_6:64

for p1, p2 being Point of (TOP-REAL 2) st LE p1,p2, rectangle ((- 1),1,(- 1),1) & p1 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & not ( p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & p2 `2 >= p1 `2 ) & not p2 in LSeg (|[(- 1),1]|,|[1,1]|) & not p2 in LSeg (|[1,1]|,|[1,(- 1)]|) holds
( p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p2 <> |[(- 1),(- 1)]| )