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 & 2 <= width G & f is_sequence_on G ) and
A2: ( 1 <= k & k + 1 <= len f ) and
A3: p in Values G and
A4: p in LSeg f,k ; :: thesis: ( p = f /. k or p = f /. (k + 1) )
A5: LSeg f,k = LSeg (f /. k),(f /. (k + 1)) by A2, TOPREAL1:def 5;
consider i, j being Element of NAT such that
A6: ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G ) and
A7: LSeg f,k c= cell G,i,j by A1, A2, Th24;
p is_extremal_in cell G,i,j by A3, A4, A6, A7, Th23;
hence ( p = f /. k or p = f /. (k + 1) ) by A4, A7, A5, SPPOL_1:def 1; :: thesis: verum