let j be Element of NAT ; :: thesis: 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; :: thesis: ( 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 A1: ( 1 <= j & j + 1 <= width G ) ; :: thesis: ((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 ;
A2: j < width G by A1, NAT_1:13;
len G <> 0 by GOBOARD1:def 5;
then A3: ( 1 <= j + 1 & 1 <= len G ) by NAT_1:11, NAT_1:14;
A4: (1 / 2) * (((G * 1,j) `1 ) + ((G * 1,j) `1 )) = (G * 1,j) `1 ;
A5: G * 1,j = |[((G * 1,j) `1 ),((G * 1,j) `2 )]| by EUCLID:57;
A6: (G * 1,1) `1 = (G * 1,j) `1 by A1, A2, A3, GOBOARD5:3;
(G * 1,1) `1 = (G * 1,(j + 1)) `1 by A1, A3, GOBOARD5:3;
then G * 1,(j + 1) = |[((G * 1,j) `1 ),((G * 1,(j + 1)) `2 )]| by A6, EUCLID:57;
then (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 A5, 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 A4, EUCLID:62;
then A7: ((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 )))]| ;
len G <> 0 by GOBOARD1:def 5;
then ( 1 <= len G & j < j + 1 ) by NAT_1:14, XREAL_1:31;
then A8: (G * 1,j) `2 < (G * 1,(j + 1)) `2 by A1, 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 A9: (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;
((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ) < ((G * 1,(j + 1)) `2 ) + ((G * 1,(j + 1)) `2 ) by A8, 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;
(G * 1,j) `1 < ((G * 1,1) `1 ) + 1 by A6, XREAL_1:31;
then A11: ((G * 1,j) `1 ) - 1 < (G * 1,1) `1 by XREAL_1:21;
( 1 <= j & j < width G ) by A1, 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 Th23;
hence ((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]| in Int (cell G,0 ,j) by A7, A9, A10, A11; :: thesis: verum