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

now

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

end;

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