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

now

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

end;

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