let j be 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 :: thesis: ex a being Element of the carrier of (TOP-REAL 2) st
( 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)) )

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:68; :: thesis: a in Int (cell (G,(len G),j))
thus a in Int (cell (G,(len G),j)) by A1, Th34; :: 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