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:8; :: 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:9; :: 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:9; :: 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:8; :: thesis: verum
end;
end;