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

now

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

end;

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