let p be Point of (TOP-REAL 2); 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; LSeg (p,((G * ((len G),1)) + |[1,(- 1)]|)) meets Int (cell (G,(len G),0))
now 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)]|;
( 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;
a in Int (cell (G,(len G),0))thus
a in Int (cell (G,(len G),0))
by Th39;
verum end;
hence
LSeg (p,((G * ((len G),1)) + |[1,(- 1)]|)) meets Int (cell (G,(len G),0))
by XBOOLE_0:3; verum