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