let p be Point of (TOP-REAL 2); ( 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
; ( 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)
; ( 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 )
;
( 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;
verum end; suppose A4:
(
p1 `1 <= 1 &
p1 `1 >= - 1 &
p1 `2 = 3 )
;
( 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
;
( 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;
verum end; suppose
|[0,3]| `1 <= p1 `1
;
( 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;
verum end; end; end; suppose
(
p1 `1 <= 1 &
p1 `1 >= - 1 &
p1 `2 = - 3 )
;
( 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;
verum end; suppose
(
p1 `1 = 1 &
p1 `2 <= 3 &
p1 `2 >= - 3 )
;
( 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;
verum end; end;