let j be Element of NAT ; for G being Go-board st 1 <= j & j + 1 <= width G holds
((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]| in Int (cell G,0 ,j)
let G be Go-board; ( 1 <= j & j + 1 <= width G implies ((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]| in Int (cell G,0 ,j) )
assume that
A1:
1 <= j
and
A2:
j + 1 <= width G
; ((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]| in Int (cell G,0 ,j)
set s1 = (G * 1,j) `2 ;
set r1 = (G * 1,j) `1 ;
set s2 = (G * 1,(j + 1)) `2 ;
len G <> 0
by GOBOARD1:def 5;
then A3:
1 <= len G
by NAT_1:14;
len G <> 0
by GOBOARD1:def 5;
then A4:
1 <= len G
by NAT_1:14;
j < j + 1
by XREAL_1:31;
then A5:
(G * 1,j) `2 < (G * 1,(j + 1)) `2
by A1, A2, A4, GOBOARD5:5;
then
((G * 1,j) `2 ) + ((G * 1,j) `2 ) < ((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 )
by XREAL_1:8;
then A6:
(1 / 2) * (((G * 1,j) `2 ) + ((G * 1,j) `2 )) < (1 / 2) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))
by XREAL_1:70;
j < width G
by A2, NAT_1:13;
then A7:
(G * 1,1) `1 = (G * 1,j) `1
by A1, A3, GOBOARD5:3;
then
(G * 1,j) `1 < ((G * 1,1) `1 ) + 1
by XREAL_1:31;
then A8:
((G * 1,j) `1 ) - 1 < (G * 1,1) `1
by XREAL_1:21;
1 <= j + 1
by NAT_1:11;
then
(G * 1,1) `1 = (G * 1,(j + 1)) `1
by A2, A3, GOBOARD5:3;
then
( G * 1,j = |[((G * 1,j) `1 ),((G * 1,j) `2 )]| & G * 1,(j + 1) = |[((G * 1,j) `1 ),((G * 1,(j + 1)) `2 )]| )
by A7, EUCLID:57;
then
( (1 / 2) * (((G * 1,j) `1 ) + ((G * 1,j) `1 )) = (G * 1,j) `1 & (G * 1,j) + (G * 1,(j + 1)) = |[(((G * 1,j) `1 ) + ((G * 1,j) `1 )),(((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))]| )
by EUCLID:60;
then
(1 / 2) * ((G * 1,j) + (G * 1,(j + 1))) = |[((G * 1,j) `1 ),((1 / 2) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 )))]|
by EUCLID:62;
then A9: ((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]| =
|[(((G * 1,j) `1 ) - 1),(((1 / 2) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))) - 0 )]|
by EUCLID:66
.=
|[(((G * 1,j) `1 ) - 1),((1 / 2) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 )))]|
;
((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ) < ((G * 1,(j + 1)) `2 ) + ((G * 1,(j + 1)) `2 )
by A5, XREAL_1:8;
then A10:
(1 / 2) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 )) < (1 / 2) * (((G * 1,(j + 1)) `2 ) + ((G * 1,(j + 1)) `2 ))
by XREAL_1:70;
j < width G
by A2, NAT_1:13;
then
Int (cell G,0 ,j) = { |[r,s]| where r, s is Real : ( r < (G * 1,1) `1 & (G * 1,j) `2 < s & s < (G * 1,(j + 1)) `2 ) }
by A1, Th23;
hence
((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]| in Int (cell G,0 ,j)
by A9, A6, A10, A8; verum