let i, j be 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:29;
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:1;
( 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, Th26;
( 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:53;
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:56;
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:58;
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:2;
(G * (1,j)) `2 = (G * (i,j)) `2 by A1, A3, A10, A12, GOBOARD5:1;
then A15: (G * (i,j)) `2 < (G * ((i + 1),(j + 1))) `2 by A3, A4, A7, A11, A5, GOBOARD5:4;
then ((G * (i,j)) `2) + ((G * (i,j)) `2) < ((G * (i,j)) `2) + ((G * ((i + 1),(j + 1))) `2) by XREAL_1:6;
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:68;
then A16: (G * (1,j)) `2 < (1 / 2) * (((G * (i,j)) `2) + ((G * ((i + 1),(j + 1))) `2)) by A1, A3, A10, A12, GOBOARD5:1;
A17: i < i + 1 by XREAL_1:29;
(G * ((i + 1),1)) `1 = (G * ((i + 1),(j + 1))) `1 by A2, A4, A6, GOBOARD5:2;
then A18: (G * (i,j)) `1 < (G * ((i + 1),(j + 1))) `1 by A1, A2, A14, A13, A17, GOBOARD5:3;
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:6;
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:68;
then A19: (1 / 2) * (((G * (i,j)) `1) + ((G * ((i + 1),(j + 1))) `1)) < (G * ((i + 1),1)) `1 by A2, A4, A6, GOBOARD5:2;
((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:6;
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:68;
then A20: (1 / 2) * (((G * (i,j)) `2) + ((G * ((i + 1),(j + 1))) `2)) < (G * (1,(j + 1))) `2 by A2, A4, A6, GOBOARD5:1;
((G * (i,j)) `1) + ((G * (i,j)) `1) < ((G * (i,j)) `1) + ((G * ((i + 1),(j + 1))) `1) by A18, XREAL_1:6;
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:68;
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