let p be Point of (TOP-REAL 2); :: thesis: ( 0 <= p `2 & p in rectangle ((- 1),1,(- 3),3) & not p in LSeg (|[(- 1),0]|,|[(- 1),3]|) & not p in LSeg (|[(- 1),3]|,|[0,3]|) & not p in LSeg (|[0,3]|,|[1,3]|) implies p in LSeg (|[1,3]|,|[1,0]|) )
assume A1: 0 <= p `2 ; :: thesis: ( not p in rectangle ((- 1),1,(- 3),3) or p in LSeg (|[(- 1),0]|,|[(- 1),3]|) or p in LSeg (|[(- 1),3]|,|[0,3]|) or p in LSeg (|[0,3]|,|[1,3]|) or p in LSeg (|[1,3]|,|[1,0]|) )
assume p in rectangle ((- 1),1,(- 3),3) ; :: thesis: ( p in LSeg (|[(- 1),0]|,|[(- 1),3]|) or p in LSeg (|[(- 1),3]|,|[0,3]|) or p in LSeg (|[0,3]|,|[1,3]|) or p in LSeg (|[1,3]|,|[1,0]|) )
then consider p1 being Point of (TOP-REAL 2) such that
A2: p1 = p and
A3: ( ( p1 `1 = - 1 & p1 `2 <= 3 & p1 `2 >= - 3 ) or ( p1 `1 <= 1 & p1 `1 >= - 1 & p1 `2 = 3 ) or ( p1 `1 <= 1 & p1 `1 >= - 1 & p1 `2 = - 3 ) or ( p1 `1 = 1 & p1 `2 <= 3 & p1 `2 >= - 3 ) ) by Lm61;
per cases ( ( p1 `1 = - 1 & p1 `2 <= 3 & p1 `2 >= - 3 ) or ( p1 `1 <= 1 & p1 `1 >= - 1 & p1 `2 = 3 ) or ( p1 `1 <= 1 & p1 `1 >= - 1 & p1 `2 = - 3 ) or ( p1 `1 = 1 & p1 `2 <= 3 & p1 `2 >= - 3 ) ) by A3;
suppose ( p1 `1 = - 1 & p1 `2 <= 3 & p1 `2 >= - 3 ) ; :: thesis: ( p in LSeg (|[(- 1),0]|,|[(- 1),3]|) or p in LSeg (|[(- 1),3]|,|[0,3]|) or p in LSeg (|[0,3]|,|[1,3]|) or p in LSeg (|[1,3]|,|[1,0]|) )
hence ( p in LSeg (|[(- 1),0]|,|[(- 1),3]|) or p in LSeg (|[(- 1),3]|,|[0,3]|) or p in LSeg (|[0,3]|,|[1,3]|) or p in LSeg (|[1,3]|,|[1,0]|) ) by A1, A2, Lm16, Lm18, Lm24, Lm25, GOBOARD7:7; :: thesis: verum
end;
suppose A4: ( p1 `1 <= 1 & p1 `1 >= - 1 & p1 `2 = 3 ) ; :: thesis: ( p in LSeg (|[(- 1),0]|,|[(- 1),3]|) or p in LSeg (|[(- 1),3]|,|[0,3]|) or p in LSeg (|[0,3]|,|[1,3]|) or p in LSeg (|[1,3]|,|[1,0]|) )
per cases ( p1 `1 <= |[0,3]| `1 or |[0,3]| `1 <= p1 `1 ) ;
suppose p1 `1 <= |[0,3]| `1 ; :: thesis: ( p in LSeg (|[(- 1),0]|,|[(- 1),3]|) or p in LSeg (|[(- 1),3]|,|[0,3]|) or p in LSeg (|[0,3]|,|[1,3]|) or p in LSeg (|[1,3]|,|[1,0]|) )
hence ( p in LSeg (|[(- 1),0]|,|[(- 1),3]|) or p in LSeg (|[(- 1),3]|,|[0,3]|) or p in LSeg (|[0,3]|,|[1,3]|) or p in LSeg (|[1,3]|,|[1,0]|) ) by A2, A4, Lm21, Lm24, Lm25, GOBOARD7:8; :: thesis: verum
end;
suppose |[0,3]| `1 <= p1 `1 ; :: thesis: ( p in LSeg (|[(- 1),0]|,|[(- 1),3]|) or p in LSeg (|[(- 1),3]|,|[0,3]|) or p in LSeg (|[0,3]|,|[1,3]|) or p in LSeg (|[1,3]|,|[1,0]|) )
hence ( p in LSeg (|[(- 1),0]|,|[(- 1),3]|) or p in LSeg (|[(- 1),3]|,|[0,3]|) or p in LSeg (|[0,3]|,|[1,3]|) or p in LSeg (|[1,3]|,|[1,0]|) ) by A2, A4, Lm21, Lm28, Lm29, GOBOARD7:8; :: thesis: verum
end;
end;
end;
suppose ( p1 `1 <= 1 & p1 `1 >= - 1 & p1 `2 = - 3 ) ; :: thesis: ( p in LSeg (|[(- 1),0]|,|[(- 1),3]|) or p in LSeg (|[(- 1),3]|,|[0,3]|) or p in LSeg (|[0,3]|,|[1,3]|) or p in LSeg (|[1,3]|,|[1,0]|) )
hence ( p in LSeg (|[(- 1),0]|,|[(- 1),3]|) or p in LSeg (|[(- 1),3]|,|[0,3]|) or p in LSeg (|[0,3]|,|[1,3]|) or p in LSeg (|[1,3]|,|[1,0]|) ) by A1, A2; :: thesis: verum
end;
suppose ( p1 `1 = 1 & p1 `2 <= 3 & p1 `2 >= - 3 ) ; :: thesis: ( p in LSeg (|[(- 1),0]|,|[(- 1),3]|) or p in LSeg (|[(- 1),3]|,|[0,3]|) or p in LSeg (|[0,3]|,|[1,3]|) or p in LSeg (|[1,3]|,|[1,0]|) )
hence ( p in LSeg (|[(- 1),0]|,|[(- 1),3]|) or p in LSeg (|[(- 1),3]|,|[0,3]|) or p in LSeg (|[0,3]|,|[1,3]|) or p in LSeg (|[1,3]|,|[1,0]|) ) by A1, A2, Lm17, Lm19, Lm28, Lm29, GOBOARD7:7; :: thesis: verum
end;
end;