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:7; :: 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: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, Lm23, Lm30, Lm31, GOBOARD7:8; :: 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:7; :: thesis: verum
end;
end;