let j be Element of NAT ; :: thesis: for p being Point of (TOP-REAL 2)
for G being Go-board st 1 <= j & j + 1 <= width G holds
LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),p meets Int (cell G,0 ,j)
let p be Point of (TOP-REAL 2); :: thesis: for G being Go-board st 1 <= j & j + 1 <= width G holds
LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),p meets Int (cell G,0 ,j)
let G be Go-board; :: thesis: ( 1 <= j & j + 1 <= width G implies LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),p meets Int (cell G,0 ,j) )
assume A1: ( 1 <= j & j + 1 <= width G ) ; :: thesis: LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),p meets Int (cell G,0 ,j)

now

take a = ((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|; :: thesis: ( a in LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),p & a in Int (cell G,0 ,j) )
thus a in LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),p by RLTOPSP1:69; :: thesis: a in Int (cell G,0 ,j)
thus a in Int (cell G,0 ,j) by A1, Th38; :: thesis: verum

end;

hence LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),p meets Int (cell G,0 ,j) by XBOOLE_0:3; :: thesis: verum