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