let j be Element of 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 GOBOARD1:def 5;
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, Th26;
len G <> 0
by GOBOARD1:def 5;
then A5:
1 <= len G
by NAT_1:14;
j < j + 1
by XREAL_1:31;
then A6:
(G * (len G),j) `2 < (G * (len G),(j + 1)) `2
by A1, A2, A5, GOBOARD5:5;
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:8;
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:70;
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:3;
then A10:
(G * (len G),1) `1 < ((G * (len G),j) `1 ) + 1
by XREAL_1:31;
A11:
1 <= j + 1
by NAT_1:11;
then
(G * (len G),1) `1 = (G * (len G),(j + 1)) `1
by A2, A3, GOBOARD5:3;
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:57;
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:60;
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:62;
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:60;
((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:8;
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:70;
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:2;
(G * 1,j) `2 = (G * (len G),j) `2
by A1, A8, A3, GOBOARD5:2;
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