let i be Nat; 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); 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; ( 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 )
; LSeg (p,(((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|)) meets Int (cell (G,i,(width G)))
now 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]|;
( 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;
a in Int (cell (G,i,(width G)))thus
a in Int (cell (G,i,(width G)))
by A1, Th32;
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; verum