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 that
A1: LE p1,p2, rectangle ((- 1),1,(- 1),1) and
A2: 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)]| ) )
( ( 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 A1, A2, Th59;
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 Th46; :: thesis: verum