let j be Nat; for G being Go-board st 1 <= j & j + 1 <= width G holds
((1 / 2) * ((G * ((len G),j)) + (G * ((len G),(j + 1))))) + |[1,0]| in Int (cell (G,(len G),j))
let G be Go-board; ( 1 <= j & j + 1 <= width G implies ((1 / 2) * ((G * ((len G),j)) + (G * ((len G),(j + 1))))) + |[1,0]| in Int (cell (G,(len G),j)) )
assume that
A1:
1 <= j
and
A2:
j + 1 <= width G
; ((1 / 2) * ((G * ((len G),j)) + (G * ((len G),(j + 1))))) + |[1,0]| in Int (cell (G,(len G),j))
set s1 = (G * ((len G),j)) `2 ;
set r1 = (G * ((len G),j)) `1 ;
set s2 = (G * ((len G),(j + 1))) `2 ;
len G <> 0
by MATRIX_0:def 10;
then A3:
1 <= len G
by NAT_1:14;
j < width G
by A2, NAT_1:13;
then A4:
Int (cell (G,(len G),j)) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 < r & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) }
by A1, Th23;
len G <> 0
by MATRIX_0:def 10;
then A5:
1 <= len G
by NAT_1:14;
j < j + 1
by XREAL_1:29;
then A6:
(G * ((len G),j)) `2 < (G * ((len G),(j + 1))) `2
by A1, A2, A5, GOBOARD5:4;
then
((G * ((len G),j)) `2) + ((G * ((len G),j)) `2) < ((G * ((len G),j)) `2) + ((G * ((len G),(j + 1))) `2)
by XREAL_1:6;
then A7:
(1 / 2) * (((G * ((len G),j)) `2) + ((G * ((len G),j)) `2)) < (1 / 2) * (((G * ((len G),j)) `2) + ((G * ((len G),(j + 1))) `2))
by XREAL_1:68;
A8:
j < width G
by A2, NAT_1:13;
then A9:
(G * ((len G),1)) `1 = (G * ((len G),j)) `1
by A1, A3, GOBOARD5:2;
then A10:
(G * ((len G),1)) `1 < ((G * ((len G),j)) `1) + 1
by XREAL_1:29;
A11:
1 <= j + 1
by NAT_1:11;
then
(G * ((len G),1)) `1 = (G * ((len G),(j + 1))) `1
by A2, A3, GOBOARD5:2;
then
( G * ((len G),j) = |[((G * ((len G),j)) `1),((G * ((len G),j)) `2)]| & G * ((len G),(j + 1)) = |[((G * ((len G),j)) `1),((G * ((len G),(j + 1))) `2)]| )
by A9, EUCLID:53;
then
( (1 / 2) * (((G * ((len G),j)) `1) + ((G * ((len G),j)) `1)) = (G * ((len G),j)) `1 & (G * ((len G),j)) + (G * ((len G),(j + 1))) = |[(((G * ((len G),j)) `1) + ((G * ((len G),j)) `1)),(((G * ((len G),j)) `2) + ((G * ((len G),(j + 1))) `2))]| )
by EUCLID:56;
then
(1 / 2) * ((G * ((len G),j)) + (G * ((len G),(j + 1)))) = |[((G * ((len G),j)) `1),((1 / 2) * (((G * ((len G),j)) `2) + ((G * ((len G),(j + 1))) `2)))]|
by EUCLID:58;
then A12:
((1 / 2) * ((G * ((len G),j)) + (G * ((len G),(j + 1))))) + |[1,0]| = |[(((G * ((len G),j)) `1) + 1),(((1 / 2) * (((G * ((len G),j)) `2) + ((G * ((len G),(j + 1))) `2))) + 0)]|
by EUCLID:56;
((G * ((len G),j)) `2) + ((G * ((len G),(j + 1))) `2) < ((G * ((len G),(j + 1))) `2) + ((G * ((len G),(j + 1))) `2)
by A6, XREAL_1:6;
then
(1 / 2) * (((G * ((len G),j)) `2) + ((G * ((len G),(j + 1))) `2)) < (1 / 2) * (((G * ((len G),(j + 1))) `2) + ((G * ((len G),(j + 1))) `2))
by XREAL_1:68;
then A13:
(1 / 2) * (((G * ((len G),j)) `2) + ((G * ((len G),(j + 1))) `2)) < (G * (1,(j + 1))) `2
by A2, A11, A3, GOBOARD5:1;
(G * (1,j)) `2 = (G * ((len G),j)) `2
by A1, A8, A3, GOBOARD5:1;
hence
((1 / 2) * ((G * ((len G),j)) + (G * ((len G),(j + 1))))) + |[1,0]| in Int (cell (G,(len G),j))
by A12, A7, A13, A10, A4; verum