let i, j be Element of NAT ; :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),p meets Int (cell G,i,j)

now

take a = (1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1))); :: thesis: ( 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:69; :: thesis: a in Int (cell G,i,j)
thus a in Int (cell G,i,j) by A1, Th34; :: thesis: 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; :: thesis: verum