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

now

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

end;

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