let G be Go-board; (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 ;
A1:
((G * ((len G),1)) `1) + 1 > (G * ((len G),1)) `1
by XREAL_1:29;
len G <> 0
by MATRIX_0:def 10;
then A2:
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)) `2 = (G * ((len G),1)) `2
by A2, GOBOARD5:1;
then
(G * ((len G),1)) `2 < ((G * (1,1)) `2) + 1
by XREAL_1:29;
then A3:
((G * ((len G),1)) `2) - 1 < (G * (1,1)) `2
by XREAL_1:19;
G * ((len G),1) = |[((G * ((len G),1)) `1),((G * ((len G),1)) `2)]|
by EUCLID:53;
then A4: (G * ((len G),1)) + |[1,(- 1)]| =
|[(((G * ((len G),1)) `1) + 1),(((G * ((len G),1)) `2) + (- 1))]|
by EUCLID:56
.=
|[(((G * ((len G),1)) `1) + 1),(((G * ((len G),1)) `2) - 1)]|
;
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 Th21;
hence
(G * ((len G),1)) + |[1,(- 1)]| in Int (cell (G,(len G),0))
by A4, A3, A1; verum