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 :: thesis: ex a being Element of the carrier of (TOP-REAL 2) st
( a in LSeg (p,((G * ((len G),1)) + |[1,(- 1)]|)) & a in Int (cell (G,(len G),0)) )
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:68; :: thesis: a in Int (cell (G,(len G),0))
thus a in Int (cell (G,(len G),0)) by Th39; :: 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