let G be Go-board; :: thesis: (G * (1,(width G))) + |[(- 1),1]| in Int (cell (G,0,(width G)))
set s1 = (G * (1,(width G))) `2 ;
set r1 = (G * (1,(width G))) `1 ;
len G <> 0 by MATRIX_0:def 10;
then A1: 1 <= len G by NAT_1:14;
width G <> 0 by MATRIX_0:def 10;
then 1 <= width G by NAT_1:14;
then (G * (1,1)) `1 = (G * (1,(width G))) `1 by A1, GOBOARD5:2;
then (G * (1,(width G))) `1 < ((G * (1,1)) `1) + 1 by XREAL_1:29;
then A2: ( ((G * (1,(width G))) `2) + 1 > (G * (1,(width G))) `2 & ((G * (1,(width G))) `1) - 1 < (G * (1,1)) `1 ) by XREAL_1:19, XREAL_1:29;
G * (1,(width G)) = |[((G * (1,(width G))) `1),((G * (1,(width G))) `2)]| by EUCLID:53;
then A3: (G * (1,(width G))) + |[(- 1),1]| = |[(((G * (1,(width G))) `1) + (- 1)),(((G * (1,(width G))) `2) + 1)]| by EUCLID:56
.= |[(((G * (1,(width G))) `1) - 1),(((G * (1,(width G))) `2) + 1)]| ;
Int (cell (G,0,(width G))) = { |[r,s]| where r, s is Real : ( r < (G * (1,1)) `1 & (G * (1,(width G))) `2 < s ) } by Th19;
hence (G * (1,(width G))) + |[(- 1),1]| in Int (cell (G,0,(width G))) by A3, A2; :: thesis: verum