let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( 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)]| implies ( p2 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & p2 <> |[(- 1),(- 1)]| ) )
set K = rectangle (- 1),1,(- 1),1;
assume ( LE p1,p2, rectangle (- 1),1,(- 1),1 & p1 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| ) ; :: thesis: ( ( p2 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & p2 `2 >= p1 `2 ) or p2 in LSeg |[(- 1),1]|,|[1,1]| or p2 in LSeg |[1,1]|,|[1,(- 1)]| or ( p2 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & p2 <> |[(- 1),(- 1)]| ) )
then ( ( p2 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[(- 1),1]|,|[1,1]| or p2 in LSeg |[1,1]|,|[1,(- 1)]| or ( p2 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & p2 <> W-min (rectangle (- 1),1,(- 1),1) ) ) by Th69;
hence ( ( p2 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & p2 `2 >= p1 `2 ) or p2 in LSeg |[(- 1),1]|,|[1,1]| or p2 in LSeg |[1,1]|,|[1,(- 1)]| or ( p2 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & p2 <> |[(- 1),(- 1)]| ) ) by Th56; :: thesis: verum