let G be Go-board; ( 1 < width G & 1 < len G implies LSeg (((G * (1,1)) - |[1,1]|),(((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)) c= ((Int (cell (G,0,0))) \/ (Int (cell (G,1,0)))) \/ {((G * (1,1)) - |[0,1]|)} )
assume that
A1:
1 < width G
and
A2:
1 < len G
; LSeg (((G * (1,1)) - |[1,1]|),(((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)) c= ((Int (cell (G,0,0))) \/ (Int (cell (G,1,0)))) \/ {((G * (1,1)) - |[0,1]|)}
set q2 = G * (1,1);
set q3 = G * (2,1);
set r = 1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1);
A3:
0 + (1 + 1) <= len G
by A2, NAT_1:13;
then A4:
(G * (1,1)) `2 = (G * (2,1)) `2
by A1, GOBOARD5:1;
(G * (1,1)) `1 < (G * (2,1)) `1
by A1, A3, GOBOARD5:3;
then A5:
((G * (2,1)) `1) - ((G * (1,1)) `1) > 0
by XREAL_1:50;
then
1 < ((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1
by XREAL_1:29, XREAL_1:129;
then A6:
1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1) < 1
by XREAL_1:212;
A7: (((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) - |[1,1]|)) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * (((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|))) `2 =
(((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) - |[1,1]|)) `2) + (((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * (((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)) `2)
by Lm1
.=
((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * (((G * (1,1)) - |[1,1]|) `2)) + (((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * (((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)) `2)
by Lm3
.=
((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * (((G * (1,1)) - |[1,1]|) `2)) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * ((((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|) `2))
by Lm3
.=
((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * (((G * (1,1)) `2) - (|[1,1]| `2))) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * ((((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|) `2))
by Lm2
.=
((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * (((G * (1,1)) `2) - (|[1,1]| `2))) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * ((((1 / 2) * ((G * (1,1)) + (G * (2,1)))) `2) - (|[0,1]| `2)))
by Lm2
.=
((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * (((G * (1,1)) `2) - 1)) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * ((((1 / 2) * ((G * (1,1)) + (G * (2,1)))) `2) - (|[0,1]| `2)))
by EUCLID:52
.=
(((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) `2)) - ((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * 1)) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * ((((1 / 2) * ((G * (1,1)) + (G * (2,1)))) `2) - 1))
by EUCLID:52
.=
(((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) `2)) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * (((1 / 2) * ((G * (1,1)) + (G * (2,1)))) `2))) - ((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) + (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)))
.=
(((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) `2)) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * ((1 / 2) * (((G * (1,1)) + (G * (2,1))) `2)))) - 1
by Lm3
.=
(((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) `2)) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * ((1 / 2) * (((G * (1,1)) `2) + ((G * (1,1)) `2))))) - 1
by A4, Lm1
.=
((G * (1,1)) `2) - (|[0,1]| `2)
by EUCLID:52
.=
((G * (1,1)) - |[0,1]|) `2
by Lm2
;
A8: (((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * ((1 / 2) * ((G * (2,1)) `1))) - ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * ((1 / 2) * ((G * (1,1)) `1)))) + (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) =
(1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)
.=
1
by A5, XCMPLX_1:106
;
(((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) - |[1,1]|)) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * (((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|))) `1 =
(((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) - |[1,1]|)) `1) + (((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * (((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)) `1)
by Lm1
.=
((((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * (G * (1,1))) - ((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * |[1,1]|)) `1) + (((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * (((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)) `1)
by RLVECT_1:34
.=
((((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * (G * (1,1))) `1) - (((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * |[1,1]|) `1)) + (((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * (((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)) `1)
by Lm2
.=
((((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * (G * (1,1))) `1) - ((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * (|[1,1]| `1))) + (((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * (((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)) `1)
by Lm3
.=
((((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * (G * (1,1))) `1) - ((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * 1)) + (((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * (((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)) `1)
by EUCLID:52
.=
(((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) `1)) - ((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * 1)) + (((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * (((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)) `1)
by Lm3
.=
(((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) `1)) - (1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)))) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * ((((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|) `1))
by Lm3
.=
(((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) `1)) - (1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)))) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * ((((1 / 2) * ((G * (1,1)) + (G * (2,1)))) `1) - (|[0,1]| `1)))
by Lm2
.=
(((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) `1)) - (1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)))) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * ((((1 / 2) * ((G * (1,1)) + (G * (2,1)))) `1) - 0))
by EUCLID:52
.=
(((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) `1)) - (1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)))) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * ((1 / 2) * (((G * (1,1)) + (G * (2,1))) `1)))
by Lm3
.=
(((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) `1)) - (1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)))) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * ((1 / 2) * (((G * (1,1)) `1) + ((G * (2,1)) `1))))
by Lm1
.=
((G * (1,1)) `1) - 0
by A8
.=
((G * (1,1)) `1) - (|[0,1]| `1)
by EUCLID:52
.=
((G * (1,1)) - |[0,1]|) `1
by Lm2
;
then ((1 - (1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1))) * ((G * (1,1)) - |[1,1]|)) + ((1 / (((1 / 2) * (((G * (2,1)) `1) - ((G * (1,1)) `1))) + 1)) * (((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)) =
|[(((G * (1,1)) - |[0,1]|) `1),(((G * (1,1)) - |[0,1]|) `2)]|
by A7, EUCLID:53
.=
(G * (1,1)) - |[0,1]|
by EUCLID:53
;
then
(G * (1,1)) - |[0,1]| in LSeg (((G * (1,1)) - |[1,1]|),(((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|))
by A5, A6;
then A9:
LSeg (((G * (1,1)) - |[1,1]|),(((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)) = (LSeg (((G * (1,1)) - |[1,1]|),((G * (1,1)) - |[0,1]|))) \/ (LSeg (((G * (1,1)) - |[0,1]|),(((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)))
by TOPREAL1:5;
set I1 = Int (cell (G,0,0));
set I2 = Int (cell (G,1,0));
(0 + 1) + 1 = 0 + (1 + 1)
;
then A10:
LSeg (((G * (1,1)) - |[0,1]|),(((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)) c= (Int (cell (G,1,0))) \/ {((G * (1,1)) - |[0,1]|)}
by A2, Th52;
A11: ((Int (cell (G,0,0))) \/ (Int (cell (G,1,0)))) \/ {((G * (1,1)) - |[0,1]|)} =
(Int (cell (G,0,0))) \/ ((Int (cell (G,1,0))) \/ ({((G * (1,1)) - |[0,1]|)} \/ {((G * (1,1)) - |[0,1]|)}))
by XBOOLE_1:4
.=
(Int (cell (G,0,0))) \/ (((Int (cell (G,1,0))) \/ {((G * (1,1)) - |[0,1]|)}) \/ {((G * (1,1)) - |[0,1]|)})
by XBOOLE_1:4
.=
((Int (cell (G,0,0))) \/ {((G * (1,1)) - |[0,1]|)}) \/ ((Int (cell (G,1,0))) \/ {((G * (1,1)) - |[0,1]|)})
by XBOOLE_1:4
;
LSeg (((G * (1,1)) - |[1,1]|),((G * (1,1)) - |[0,1]|)) c= (Int (cell (G,0,0))) \/ {((G * (1,1)) - |[0,1]|)}
by Th60;
hence
LSeg (((G * (1,1)) - |[1,1]|),(((1 / 2) * ((G * (1,1)) + (G * (2,1)))) - |[0,1]|)) c= ((Int (cell (G,0,0))) \/ (Int (cell (G,1,0)))) \/ {((G * (1,1)) - |[0,1]|)}
by A9, A10, A11, XBOOLE_1:13; verum