let p be Point of (TOP-REAL 2); :: thesis: for G being Go-board holds LSeg (p,((G * (1,(width G))) + |[(- 1),1]|)) meets Int (cell (G,0,(width G)))
let G be Go-board; :: thesis: LSeg (p,((G * (1,(width G))) + |[(- 1),1]|)) meets Int (cell (G,0,(width G)))

now :: thesis: ex a being Element of the carrier of (TOP-REAL 2) st
( a in LSeg (p,((G * (1,(width G))) + |[(- 1),1]|)) & a in Int (cell (G,0,(width G))) )

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

end;

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