let G be Go-board; (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:53;
then A1:
(G * (1,1)) - |[1,1]| = |[(((G * (1,1)) `1) - 1),(((G * (1,1)) `2) - 1)]|
by EUCLID:62;
(G * (1,1)) `2 < ((G * (1,1)) `2) + 1
by XREAL_1:29;
then A2:
((G * (1,1)) `2) - 1 < (G * (1,1)) `2
by XREAL_1:19;
(G * (1,1)) `1 < ((G * (1,1)) `1) + 1
by XREAL_1:29;
then A3:
((G * (1,1)) `1) - 1 < (G * (1,1)) `1
by XREAL_1:19;
Int (cell (G,0,0)) = { |[r,s]| where r, s is Real : ( r < (G * (1,1)) `1 & s < (G * (1,1)) `2 ) }
by Th18;
hence
(G * (1,1)) - |[1,1]| in Int (cell (G,0,0))
by A1, A2, A3; verum