let j, i be Element of NAT ; for G being Go-board st 1 <= j & j < width G & 1 <= i & i + 1 < len G holds
LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) c= ((Int (cell G,i,j)) \/ (Int (cell G,(i + 1),j))) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}
let G be Go-board; ( 1 <= j & j < width G & 1 <= i & i + 1 < len G implies LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) c= ((Int (cell G,i,j)) \/ (Int (cell G,(i + 1),j))) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))} )
assume that
A1:
1 <= j
and
A2:
j < width G
and
A3:
1 <= i
and
A4:
i + 1 < len G
; LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) c= ((Int (cell G,i,j)) \/ (Int (cell G,(i + 1),j))) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}
set p1 = G * i,j;
set p2 = G * (i + 1),j;
set q2 = G * (i + 1),(j + 1);
set q3 = G * (i + 2),(j + 1);
set r = (((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ));
A5:
i + 1 >= 1
by NAT_1:11;
set I1 = Int (cell G,i,j);
set I2 = Int (cell G,(i + 1),j);
i <= i + 1
by NAT_1:11;
then A6:
i < len G
by A4, XXREAL_0:2;
then A7:
LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1)))) c= (Int (cell G,i,j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}
by A1, A2, A3, Th45;
i < i + 1
by XREAL_1:31;
then
(G * i,j) `1 < (G * (i + 1),j) `1
by A1, A2, A3, A4, GOBOARD5:4;
then A8:
((G * (i + 1),j) `1 ) - ((G * i,j) `1 ) > 0
by XREAL_1:52;
A9:
(i + 1) + 1 = i + (1 + 1)
;
then A10:
i + 2 >= 1
by NAT_1:11;
A11:
i + (1 + 1) <= len G
by A4, A9, NAT_1:13;
A12:
( j + 1 >= 1 & j + 1 <= width G )
by A2, NAT_1:11, NAT_1:13;
then A13: (G * (i + 1),(j + 1)) `2 =
(G * 1,(j + 1)) `2
by A4, A5, GOBOARD5:2
.=
(G * (i + 2),(j + 1)) `2
by A11, A10, A12, GOBOARD5:2
;
A14: (G * (i + 1),(j + 1)) `1 =
(G * (i + 1),1) `1
by A4, A5, A12, GOBOARD5:3
.=
(G * (i + 1),j) `1
by A1, A2, A4, A5, GOBOARD5:3
;
i + 1 < i + 2
by XREAL_1:8;
then
(G * (i + 1),(j + 1)) `1 < (G * (i + 2),(j + 1)) `1
by A5, A11, A12, GOBOARD5:4;
then A15:
((G * (i + 1),j) `1 ) - ((G * i,j) `1 ) < ((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )
by A14, XREAL_1:11;
then A16:
((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )) = ((G * (i + 1),j) `1 ) - ((G * i,j) `1 )
by A8, XCMPLX_1:88;
(G * i,j) `2 =
(G * 1,j) `2
by A1, A2, A3, A6, GOBOARD5:2
.=
(G * (i + 1),j) `2
by A1, A2, A4, A5, GOBOARD5:2
;
then A17: ((G * (i + 1),j) + (G * (i + 1),(j + 1))) `2 =
((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) `2 ) + ((G * (i + 1),(j + 1)) `2 ))) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * (((G * (i + 1),j) `2 ) + ((G * (i + 2),(j + 1)) `2 )))
by A13, Lm1
.=
((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) + (G * (i + 1),(j + 1))) `2 )) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * (((G * (i + 1),j) `2 ) + ((G * (i + 2),(j + 1)) `2 )))
by Lm1
.=
((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) + (G * (i + 1),(j + 1))) `2 )) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * (((G * (i + 1),j) + (G * (i + 2),(j + 1))) `2 ))
by Lm1
.=
((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) + (G * (i + 1),(j + 1))) `2 )) + ((((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) `2 )
by Lm3
.=
(((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((G * i,j) + (G * (i + 1),(j + 1)))) `2 ) + ((((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) `2 )
by Lm3
.=
(((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((G * i,j) + (G * (i + 1),(j + 1)))) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1))))) `2
by Lm1
;
((G * (i + 1),j) + (G * (i + 1),(j + 1))) `1 =
((G * (i + 1),j) `1 ) + ((((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) + (1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))))) * ((G * (i + 1),(j + 1)) `1 ))
by Lm1
.=
((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) `1 ) + ((G * (i + 1),(j + 1)) `1 ))) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * (((G * (i + 1),j) `1 ) + ((G * (i + 2),(j + 1)) `1 )))
by A14, A16
.=
((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) `1 ) + ((G * (i + 1),(j + 1)) `1 ))) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * (((G * (i + 1),j) + (G * (i + 2),(j + 1))) `1 ))
by Lm1
.=
((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) + (G * (i + 1),(j + 1))) `1 )) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * (((G * (i + 1),j) + (G * (i + 2),(j + 1))) `1 ))
by Lm1
.=
((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) + (G * (i + 1),(j + 1))) `1 )) + ((((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) `1 )
by Lm3
.=
(((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((G * i,j) + (G * (i + 1),(j + 1)))) `1 ) + ((((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) `1 )
by Lm3
.=
(((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((G * i,j) + (G * (i + 1),(j + 1)))) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1))))) `1
by Lm1
;
then ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((G * i,j) + (G * (i + 1),(j + 1)))) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) =
|[(((G * (i + 1),j) + (G * (i + 1),(j + 1))) `1 ),(((G * (i + 1),j) + (G * (i + 1),(j + 1))) `2 )]|
by A17, EUCLID:57
.=
(G * (i + 1),j) + (G * (i + 1),(j + 1))
by EUCLID:57
;
then A18: (1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))) =
((1 / 2) * ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((G * i,j) + (G * (i + 1),(j + 1))))) + ((1 / 2) * (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))))
by EUCLID:36
.=
(((1 / 2) * (1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))))) * ((G * i,j) + (G * (i + 1),(j + 1)))) + ((1 / 2) * (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))))
by EUCLID:34
.=
((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1))))) + ((1 / 2) * (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))))
by EUCLID:34
.=
((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1))))) + (((1 / 2) * ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1))))
by EUCLID:34
.=
((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1))))) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((1 / 2) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))))
by EUCLID:34
;
(((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )) < 1
by A15, A8, XREAL_1:191;
then
(1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))) in LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 2),(j + 1))))
by A15, A8, A18;
then A19:
LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) = (LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))) \/ (LSeg ((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))))
by TOPREAL1:11;
A20: ((Int (cell G,i,j)) \/ (Int (cell G,(i + 1),j))) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))} =
(Int (cell G,i,j)) \/ ((Int (cell G,(i + 1),j)) \/ ({((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))} \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}))
by XBOOLE_1:4
.=
(Int (cell G,i,j)) \/ (((Int (cell G,(i + 1),j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))})
by XBOOLE_1:4
.=
((Int (cell G,i,j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}) \/ ((Int (cell G,(i + 1),j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))})
by XBOOLE_1:4
;
LSeg ((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) c= (Int (cell G,(i + 1),j)) \/ {((1 / 2) * ((G * (i + 1),j) + (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 + 1),j) + (G * (i + 2),(j + 1)))) c= ((Int (cell G,i,j)) \/ (Int (cell G,(i + 1),j))) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}
by A19, A7, A20, XBOOLE_1:13; verum