let G be Go-board; :: thesis: (G * (len G),1) + |[1,(- 1)]| in Int (cell G,(len G),0 )
set s1 = (G * (len G),1) `2 ;
set r1 = (G * (len G),1) `1 ;
width G <> 0 by GOBOARD1:def 5;
then A1: 1 <= width G by NAT_1:14;
len G <> 0 by GOBOARD1:def 5;
then 1 <= len G by NAT_1:14;
then A2: (G * 1,1) `2 = (G * (len G),1) `2 by A1, GOBOARD5:2;
G * (len G),1 = |[((G * (len G),1) `1 ),((G * (len G),1) `2 )]| by EUCLID:57;
then A3: (G * (len G),1) + |[1,(- 1)]| = |[(((G * (len G),1) `1 ) + 1),(((G * (len G),1) `2 ) + (- 1))]| by EUCLID:60
.= |[(((G * (len G),1) `1 ) + 1),(((G * (len G),1) `2 ) - 1)]| ;
(G * (len G),1) `2 < ((G * 1,1) `2 ) + 1 by A2, XREAL_1:31;
then A4: ((G * (len G),1) `2 ) - 1 < (G * 1,1) `2 by XREAL_1:21;
A5: ((G * (len G),1) `1 ) + 1 > (G * (len G),1) `1 by XREAL_1:31;
Int (cell G,(len G),0 ) = { |[r,s]| where r, s is Real : ( (G * (len G),1) `1 < r & s < (G * 1,1) `2 ) } by Th24;
hence (G * (len G),1) + |[1,(- 1)]| in Int (cell G,(len G),0 ) by A3, A4, A5; :: thesis: verum