for i, j, k being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (j,i)),(G * (k,i))) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k holds
ex n being Nat st
( j <= n & n <= k & (G * (n,i)) `1 = lower_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )