let k be 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 3;
consider i, j being 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, Th22;
p is_extremal_in cell (G,i,j) by A3, A4, A6, A7, Th21;
hence ( p = f /. k or p = f /. (k + 1) ) by A4, A7, A5, SPPOL_1:def 1; :: thesis: verum