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