let i, j be Nat; for p being Point of (TOP-REAL 2)
for G being Go-board st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),p) meets Int (cell (G,i,j))
let p be Point of (TOP-REAL 2); for G being Go-board st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),p) meets Int (cell (G,i,j))
let G be Go-board; ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G implies LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),p) meets Int (cell (G,i,j)) )
assume A1:
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G )
; LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),p) meets Int (cell (G,i,j))
now ex a being Element of the carrier of (TOP-REAL 2) st
( a in LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),p) & a in Int (cell (G,i,j)) )take a =
(1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))));
( a in LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),p) & a in Int (cell (G,i,j)) )thus
a in LSeg (
((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),
p)
by RLTOPSP1:68;
a in Int (cell (G,i,j))thus
a in Int (cell (G,i,j))
by A1, Th31;
verum end;
hence
LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),p) meets Int (cell (G,i,j))
by XBOOLE_0:3; verum