let G be Go-board; :: thesis: (G * 1,1) - |[1,1]| in Int (cell G,0 ,0 )
set s1 = (G * 1,1) `2 ;
set r1 = (G * 1,1) `1 ;
G * 1,1 = |[((G * 1,1) `1 ),((G * 1,1) `2 )]| by EUCLID:57;
then A1: (G * 1,1) - |[1,1]| = |[(((G * 1,1) `1 ) - 1),(((G * 1,1) `2 ) - 1)]| by EUCLID:66;
(G * 1,1) `2 < ((G * 1,1) `2 ) + 1 by XREAL_1:31;
then A2: ((G * 1,1) `2 ) - 1 < (G * 1,1) `2 by XREAL_1:21;
(G * 1,1) `1 < ((G * 1,1) `1 ) + 1 by XREAL_1:31;
then A3: ((G * 1,1) `1 ) - 1 < (G * 1,1) `1 by XREAL_1:21;
Int (cell G,0 ,0 ) = { |[r,s]| where r, s is Real : ( r < (G * 1,1) `1 & s < (G * 1,1) `2 ) } by Th21;
hence (G * 1,1) - |[1,1]| in Int (cell G,0 ,0 ) by A1, A2, A3; :: thesis: verum