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

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:69; :: thesis: a in Int (cell G,0 ,(width G))
thus a in Int (cell G,0 ,(width G)) by Th41; :: 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