let i, j be Element of NAT ; :: thesis: for G being Go-board st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
(1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1))) in Int (cell G,i,j)
let G be Go-board; :: thesis: ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G implies (1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1))) in Int (cell G,i,j) )
assume that
A1: 1 <= i and
A2: i + 1 <= len G and
A3: 1 <= j and
A4: j + 1 <= width G ; :: thesis: (1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1))) in Int (cell G,i,j)
A5: j < j + 1 by XREAL_1:31;
set r1 = (G * i,j) `1 ;
set s1 = (G * i,j) `2 ;
set r2 = (G * (i + 1),(j + 1)) `1 ;
set s2 = (G * (i + 1),(j + 1)) `2 ;
A6: ( 1 <= i + 1 & 1 <= j + 1 ) by NAT_1:11;
then A7: (G * 1,(j + 1)) `2 = (G * (i + 1),(j + 1)) `2 by A2, A4, GOBOARD5:2;
( i < len G & j < width G ) by A2, A4, NAT_1:13;
then A8: Int (cell G,i,j) = { |[r,s]| where r, s is Real : ( (G * i,1) `1 < r & r < (G * (i + 1),1) `1 & (G * 1,j) `2 < s & s < (G * 1,(j + 1)) `2 ) } by A1, A3, Th29;
( G * i,j = |[((G * i,j) `1 ),((G * i,j) `2 )]| & G * (i + 1),(j + 1) = |[((G * (i + 1),(j + 1)) `1 ),((G * (i + 1),(j + 1)) `2 )]| ) by EUCLID:57;
then (G * i,j) + (G * (i + 1),(j + 1)) = |[(((G * i,j) `1 ) + ((G * (i + 1),(j + 1)) `1 )),(((G * i,j) `2 ) + ((G * (i + 1),(j + 1)) `2 ))]| by EUCLID:60;
then A9: (1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1))) = |[((1 / 2) * (((G * i,j) `1 ) + ((G * (i + 1),(j + 1)) `1 ))),((1 / 2) * (((G * i,j) `2 ) + ((G * (i + 1),(j + 1)) `2 )))]| by EUCLID:62;
i <= i + 1 by NAT_1:11;
then A10: i <= len G by A2, XXREAL_0:2;
then A11: 1 <= len G by A1, XXREAL_0:2;
j <= j + 1 by NAT_1:11;
then A12: j <= width G by A4, XXREAL_0:2;
then A13: 1 <= width G by A3, XXREAL_0:2;
A14: (G * i,1) `1 = (G * i,j) `1 by A1, A3, A10, A12, GOBOARD5:3;
(G * 1,j) `2 = (G * i,j) `2 by A1, A3, A10, A12, GOBOARD5:2;
then A15: (G * i,j) `2 < (G * (i + 1),(j + 1)) `2 by A3, A4, A7, A11, A5, GOBOARD5:5;
then ((G * i,j) `2 ) + ((G * i,j) `2 ) < ((G * i,j) `2 ) + ((G * (i + 1),(j + 1)) `2 ) by XREAL_1:8;
then (1 / 2) * (((G * i,j) `2 ) + ((G * i,j) `2 )) < (1 / 2) * (((G * i,j) `2 ) + ((G * (i + 1),(j + 1)) `2 )) by XREAL_1:70;
then A16: (G * 1,j) `2 < (1 / 2) * (((G * i,j) `2 ) + ((G * (i + 1),(j + 1)) `2 )) by A1, A3, A10, A12, GOBOARD5:2;
A17: i < i + 1 by XREAL_1:31;
(G * (i + 1),1) `1 = (G * (i + 1),(j + 1)) `1 by A2, A4, A6, GOBOARD5:3;
then A18: (G * i,j) `1 < (G * (i + 1),(j + 1)) `1 by A1, A2, A14, A13, A17, GOBOARD5:4;
then ((G * i,j) `1 ) + ((G * (i + 1),(j + 1)) `1 ) < ((G * (i + 1),(j + 1)) `1 ) + ((G * (i + 1),(j + 1)) `1 ) by XREAL_1:8;
then (1 / 2) * (((G * i,j) `1 ) + ((G * (i + 1),(j + 1)) `1 )) < (1 / 2) * (((G * (i + 1),(j + 1)) `1 ) + ((G * (i + 1),(j + 1)) `1 )) by XREAL_1:70;
then A19: (1 / 2) * (((G * i,j) `1 ) + ((G * (i + 1),(j + 1)) `1 )) < (G * (i + 1),1) `1 by A2, A4, A6, GOBOARD5:3;
((G * i,j) `2 ) + ((G * (i + 1),(j + 1)) `2 ) < ((G * (i + 1),(j + 1)) `2 ) + ((G * (i + 1),(j + 1)) `2 ) by A15, XREAL_1:8;
then (1 / 2) * (((G * i,j) `2 ) + ((G * (i + 1),(j + 1)) `2 )) < (1 / 2) * (((G * (i + 1),(j + 1)) `2 ) + ((G * (i + 1),(j + 1)) `2 )) by XREAL_1:70;
then A20: (1 / 2) * (((G * i,j) `2 ) + ((G * (i + 1),(j + 1)) `2 )) < (G * 1,(j + 1)) `2 by A2, A4, A6, GOBOARD5:2;
((G * i,j) `1 ) + ((G * i,j) `1 ) < ((G * i,j) `1 ) + ((G * (i + 1),(j + 1)) `1 ) by A18, XREAL_1:8;
then (1 / 2) * (((G * i,j) `1 ) + ((G * i,j) `1 )) < (1 / 2) * (((G * i,j) `1 ) + ((G * (i + 1),(j + 1)) `1 )) by XREAL_1:70;
hence (1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1))) in Int (cell G,i,j) by A9, A14, A19, A16, A20, A8; :: thesis: verum