let i be 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 :: thesis: ex a being Element of the carrier of (TOP-REAL 2) st
( 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))) )

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:68; :: thesis: a in Int (cell (G,i,(width G)))
thus a in Int (cell (G,i,(width G))) by A1, Th32; :: 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