let i, j be Nat; for G being Go-board st 1 <= i & i < len G & 1 <= j & j + 1 < width G holds
LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2)))))) c= ((Int (cell (G,i,j))) \/ (Int (cell (G,i,(j + 1))))) \/ {((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))))}
let G be Go-board; ( 1 <= i & i < len G & 1 <= j & j + 1 < width G implies LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2)))))) c= ((Int (cell (G,i,j))) \/ (Int (cell (G,i,(j + 1))))) \/ {((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))))} )
assume that
A1:
1 <= i
and
A2:
i < len G
and
A3:
1 <= j
and
A4:
j + 1 < width G
; LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2)))))) c= ((Int (cell (G,i,j))) \/ (Int (cell (G,i,(j + 1))))) \/ {((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))))}
set p1 = G * (i,j);
set p2 = G * (i,(j + 1));
set q2 = G * ((i + 1),(j + 1));
set q3 = G * ((i + 1),(j + 2));
set r = (((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2));
A5:
j + 1 >= 1
by NAT_1:11;
set I1 = Int (cell (G,i,j));
set I2 = Int (cell (G,i,(j + 1)));
j <= j + 1
by NAT_1:11;
then A6:
j < width G
by A4, XXREAL_0:2;
then A7:
LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))))) c= (Int (cell (G,i,j))) \/ {((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))))}
by A1, A2, A3, Th41;
j < j + 1
by XREAL_1:29;
then
(G * (i,j)) `2 < (G * (i,(j + 1))) `2
by A1, A2, A3, A4, GOBOARD5:4;
then A8:
((G * (i,(j + 1))) `2) - ((G * (i,j)) `2) > 0
by XREAL_1:50;
A9:
(j + 1) + 1 = j + (1 + 1)
;
then A10:
j + 2 >= 1
by NAT_1:11;
A11:
j + (1 + 1) <= width G
by A4, A9, NAT_1:13;
A12:
( i + 1 >= 1 & i + 1 <= len G )
by A2, NAT_1:11, NAT_1:13;
then A13: (G * ((i + 1),(j + 1))) `1 =
(G * ((i + 1),1)) `1
by A4, A5, GOBOARD5:2
.=
(G * ((i + 1),(j + 2))) `1
by A11, A10, A12, GOBOARD5:2
;
A14: (G * ((i + 1),(j + 1))) `2 =
(G * (1,(j + 1))) `2
by A4, A5, A12, GOBOARD5:1
.=
(G * (i,(j + 1))) `2
by A1, A2, A4, A5, GOBOARD5:1
;
j + 1 < j + 2
by XREAL_1:6;
then
(G * ((i + 1),(j + 1))) `2 < (G * ((i + 1),(j + 2))) `2
by A5, A11, A12, GOBOARD5:4;
then A15:
((G * (i,(j + 1))) `2) - ((G * (i,j)) `2) < ((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)
by A14, XREAL_1:9;
then A16:
((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)) = ((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)
by A8, XCMPLX_1:87;
(G * (i,j)) `1 =
(G * (i,1)) `1
by A1, A2, A3, A6, GOBOARD5:2
.=
(G * (i,(j + 1))) `1
by A1, A2, A4, A5, GOBOARD5:2
;
then A17: ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))) `1 =
((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * (((G * (i,j)) `1) + ((G * ((i + 1),(j + 1))) `1))) + (((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * (((G * (i,(j + 1))) `1) + ((G * ((i + 1),(j + 2))) `1)))
by A13, Lm1
.=
((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * (((G * (i,j)) + (G * ((i + 1),(j + 1)))) `1)) + (((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * (((G * (i,(j + 1))) `1) + ((G * ((i + 1),(j + 2))) `1)))
by Lm1
.=
((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * (((G * (i,j)) + (G * ((i + 1),(j + 1)))) `1)) + (((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * (((G * (i,(j + 1))) + (G * ((i + 1),(j + 2)))) `1))
by Lm1
.=
((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * (((G * (i,j)) + (G * ((i + 1),(j + 1)))) `1)) + ((((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2))))) `1)
by Lm3
.=
(((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) `1) + ((((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2))))) `1)
by Lm3
.=
(((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) + (((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2)))))) `1
by Lm1
;
((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))) `2 =
((G * (i,(j + 1))) `2) + ((((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) + (1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))))) * ((G * ((i + 1),(j + 1))) `2))
by Lm1
.=
((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * (((G * (i,j)) `2) + ((G * ((i + 1),(j + 1))) `2))) + (((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * (((G * (i,(j + 1))) `2) + ((G * ((i + 1),(j + 2))) `2)))
by A14, A16
.=
((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * (((G * (i,j)) `2) + ((G * ((i + 1),(j + 1))) `2))) + (((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * (((G * (i,(j + 1))) + (G * ((i + 1),(j + 2)))) `2))
by Lm1
.=
((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * (((G * (i,j)) + (G * ((i + 1),(j + 1)))) `2)) + (((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * (((G * (i,(j + 1))) + (G * ((i + 1),(j + 2)))) `2))
by Lm1
.=
((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * (((G * (i,j)) + (G * ((i + 1),(j + 1)))) `2)) + ((((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2))))) `2)
by Lm3
.=
(((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) `2) + ((((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2))))) `2)
by Lm3
.=
(((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) + (((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2)))))) `2
by Lm1
;
then ((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) + (((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2))))) =
|[(((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))) `1),(((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))) `2)]|
by A17, EUCLID:53
.=
(G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))
by EUCLID:53
;
then A18: (1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))) =
((1 / 2) * ((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))))) + ((1 / 2) * (((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2))))))
by RLVECT_1:def 5
.=
(((1 / 2) * (1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))))) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) + ((1 / 2) * (((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2))))))
by RLVECT_1:def 7
.=
((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * ((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))))) + ((1 / 2) * (((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2))))))
by RLVECT_1:def 7
.=
((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * ((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))))) + (((1 / 2) * ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2)))))
by RLVECT_1:def 7
.=
((1 - ((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)))) * ((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))))) + (((((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2))) * ((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2))))))
by RLVECT_1:def 7
;
(((G * (i,(j + 1))) `2) - ((G * (i,j)) `2)) / (((G * ((i + 1),(j + 2))) `2) - ((G * (i,j)) `2)) < 1
by A15, A8, XREAL_1:189;
then
(1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))) in LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2))))))
by A15, A8, A18;
then A19:
LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2)))))) = (LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1))))))) \/ (LSeg (((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1))))),((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2)))))))
by TOPREAL1:5;
A20: ((Int (cell (G,i,j))) \/ (Int (cell (G,i,(j + 1))))) \/ {((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))))} =
(Int (cell (G,i,j))) \/ ((Int (cell (G,i,(j + 1)))) \/ ({((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))))} \/ {((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))))}))
by XBOOLE_1:4
.=
(Int (cell (G,i,j))) \/ (((Int (cell (G,i,(j + 1)))) \/ {((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))))}) \/ {((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))))})
by XBOOLE_1:4
.=
((Int (cell (G,i,j))) \/ {((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))))}) \/ ((Int (cell (G,i,(j + 1)))) \/ {((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))))})
by XBOOLE_1:4
;
LSeg (((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1))))),((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2)))))) c= (Int (cell (G,i,(j + 1)))) \/ {((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))))}
by A1, A2, A4, A5, A9, Th43;
hence
LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 2)))))) c= ((Int (cell (G,i,j))) \/ (Int (cell (G,i,(j + 1))))) \/ {((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1)))))}
by A19, A7, A20, XBOOLE_1:13; verum