let p be Point of (TOP-REAL 2); :: thesis: ( p `2 <= 0 & 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: p `2 <= 0 ; :: 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, Lm26, Lm27, GOBOARD7:8; :: thesis: verum
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 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, Lm23, Lm26, Lm27, 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, Lm23, Lm30, Lm31, GOBOARD7:9; :: thesis: verum
end;
end;
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, Lm30, Lm31, GOBOARD7:8; :: thesis: verum
end;
end;