let i be Element of 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 GOBOARD1:def 5;
then A3: 1 <= width G by NAT_1:14;
width G <> 0 by GOBOARD1:def 5;
then A4: 1 <= width G by NAT_1:14;
i < i + 1 by XREAL_1:31;
then A5: (G * i,1) `1 < (G * (i + 1),1) `1 by A1, A2, A4, GOBOARD5:4;
then ((G * i,1) `1 ) + ((G * i,1) `1 ) < ((G * i,1) `1 ) + ((G * (i + 1),1) `1 ) by XREAL_1:8;
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:70;
i < len G by A2, NAT_1:13;
then A7: (G * 1,1) `2 = (G * i,1) `2 by A1, A3, GOBOARD5:2;
then (G * i,1) `2 < ((G * 1,1) `2 ) + 1 by XREAL_1:31;
then A8: ((G * i,1) `2 ) - 1 < (G * 1,1) `2 by XREAL_1:21;
1 <= i + 1 by NAT_1:11;
then (G * 1,1) `2 = (G * (i + 1),1) `2 by A2, A3, GOBOARD5:2;
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:57;
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:60;
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:62;
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:66
.= |[((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:8;
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:70;
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, Th27;
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