let G be Go-board; (G * ((len G),(width G))) + |[1,1]| in Int (cell (G,(len G),(width G)))
set s1 = (G * ((len G),(width G))) `2 ;
set r1 = (G * ((len G),(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 A2:
1 <= width G
by NAT_1:14;
then
(G * ((len G),1)) `1 = (G * ((len G),(width G))) `1
by A1, GOBOARD5:2;
then A3:
((G * ((len G),(width G))) `1) + 1 > (G * ((len G),1)) `1
by XREAL_1:29;
G * ((len G),(width G)) = |[((G * ((len G),(width G))) `1),((G * ((len G),(width G))) `2)]|
by EUCLID:53;
then A4:
(G * ((len G),(width G))) + |[1,1]| = |[(((G * ((len G),(width G))) `1) + 1),(((G * ((len G),(width G))) `2) + 1)]|
by EUCLID:56;
(G * (1,(width G))) `2 = (G * ((len G),(width G))) `2
by A2, A1, GOBOARD5:1;
then A5:
((G * ((len G),(width G))) `2) + 1 > (G * (1,(width G))) `2
by XREAL_1:29;
Int (cell (G,(len G),(width G))) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 < r & (G * (1,(width G))) `2 < s ) }
by Th22;
hence
(G * ((len G),(width G))) + |[1,1]| in Int (cell (G,(len G),(width G)))
by A4, A5, A3; verum