let G be Go-board; :: thesis: (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 ;
width G <> 0 by GOBOARD1:def 5;
then A1: 1 <= width G by NAT_1:14;
len G <> 0 by GOBOARD1:def 5;
then A2: 1 <= len G by NAT_1:14;
then A3: (G * (len G),1) `1 = (G * (len G),(width G)) `1 by A1, GOBOARD5:3;
A4: (G * 1,(width G)) `2 = (G * (len G),(width G)) `2 by A1, A2, GOBOARD5:2;
G * (len G),(width G) = |[((G * (len G),(width G)) `1 ),((G * (len G),(width G)) `2 )]| by EUCLID:57;
then A5: (G * (len G),(width G)) + |[1,1]| = |[(((G * (len G),(width G)) `1 ) + 1),(((G * (len G),(width G)) `2 ) + 1)]| by EUCLID:60;
A6: ((G * (len G),(width G)) `2 ) + 1 > (G * 1,(width G)) `2 by A4, XREAL_1:31;
A7: ((G * (len G),(width G)) `1 ) + 1 > (G * (len G),1) `1 by A3, XREAL_1:31;
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 Th25;
hence (G * (len G),(width G)) + |[1,1]| in Int (cell G,(len G),(width G)) by A5, A6, A7; :: thesis: verum