let j be Nat; :: thesis: for p being Point of (TOP-REAL 2)
for G being Go-board st 1 <= j & j + 1 <= width G holds
LSeg ((((1 / 2) * ((G * (1,j)) + (G * (1,(j + 1))))) - |[1,0]|),p) meets Int (cell (G,0,j))
let p be Point of (TOP-REAL 2); :: thesis: for G being Go-board st 1 <= j & j + 1 <= width G holds
LSeg ((((1 / 2) * ((G * (1,j)) + (G * (1,(j + 1))))) - |[1,0]|),p) meets Int (cell (G,0,j))
let G be Go-board; :: thesis: ( 1 <= j & j + 1 <= width G implies LSeg ((((1 / 2) * ((G * (1,j)) + (G * (1,(j + 1))))) - |[1,0]|),p) meets Int (cell (G,0,j)) )
assume A1: ( 1 <= j & j + 1 <= width G ) ; :: thesis: LSeg ((((1 / 2) * ((G * (1,j)) + (G * (1,(j + 1))))) - |[1,0]|),p) meets Int (cell (G,0,j))

now :: thesis: ex a being Element of the carrier of (TOP-REAL 2) st
( a in LSeg ((((1 / 2) * ((G * (1,j)) + (G * (1,(j + 1))))) - |[1,0]|),p) & a in Int (cell (G,0,j)) )

take a = ((1 / 2) * ((G * (1,j)) + (G * (1,(j + 1))))) - |[1,0]|; :: thesis: ( a in LSeg ((((1 / 2) * ((G * (1,j)) + (G * (1,(j + 1))))) - |[1,0]|),p) & a in Int (cell (G,0,j)) )
thus a in LSeg ((((1 / 2) * ((G * (1,j)) + (G * (1,(j + 1))))) - |[1,0]|),p) by RLTOPSP1:68; :: thesis: a in Int (cell (G,0,j))
thus a in Int (cell (G,0,j)) by A1, Th35; :: thesis: verum

end;

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