let k be Element of NAT ; :: thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st 2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k + 1 <= len f & p in Values G & p in LSeg f,k & not p = f /. k holds
p = f /. (k + 1)
let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st 2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k + 1 <= len f & p in Values G & p in LSeg f,k & not p = f /. k holds
p = f /. (k + 1)
let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st 2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k + 1 <= len f & p in Values G & p in LSeg f,k & not p = f /. k holds
p = f /. (k + 1)
let p be Point of (TOP-REAL 2); :: thesis: ( 2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k + 1 <= len f & p in Values G & p in LSeg f,k & not p = f /. k implies p = f /. (k + 1) )
assume that
A1: 2 <= len G and
A2: 2 <= width G and
A3: f is_sequence_on G and
A4: 1 <= k and
A5: k + 1 <= len f and
A6: p in Values G and
A7: p in LSeg f,k ; :: thesis: ( p = f /. k or p = f /. (k + 1) )
consider i, j being Element of NAT such that
A8: ( 1 <= i & i + 1 <= len G ) and
A9: ( 1 <= j & j + 1 <= width G ) and
A10: LSeg f,k c= cell G,i,j by A1, A2, A3, A4, A5, Th24;
A11: LSeg f,k = LSeg (f /. k),(f /. (k + 1)) by A4, A5, TOPREAL1:def 5;
p is_extremal_in cell G,i,j by A6, A7, A8, A9, A10, Th23;
hence ( p = f /. k or p = f /. (k + 1) ) by A7, A10, A11, SPPOL_1:def 1; :: thesis: verum