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 ;
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) `1 = (G * 1,(width G)) `1 by A1, GOBOARD5:3;
G * 1,(width G) = |[((G * 1,(width G)) `1 ),((G * 1,(width G)) `2 )]| by EUCLID:57;
then A3: (G * 1,(width G)) + |[(- 1),1]| = |[(((G * 1,(width G)) `1 ) + (- 1)),(((G * 1,(width G)) `2 ) + 1)]| by EUCLID:60
.= |[(((G * 1,(width G)) `1 ) - 1),(((G * 1,(width G)) `2 ) + 1)]| ;
A4: ((G * 1,(width G)) `2 ) + 1 > (G * 1,(width G)) `2 by XREAL_1:31;
(G * 1,(width G)) `1 < ((G * 1,1) `1 ) + 1 by A2, XREAL_1:31;
then A5: ((G * 1,(width G)) `1 ) - 1 < (G * 1,1) `1 by XREAL_1:21;
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 Th22;
hence (G * 1,(width G)) + |[(- 1),1]| in Int (cell G,0 ,(width G)) by A3, A4, A5; :: thesis: verum