let k be Nat; :: thesis: for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

right_cell (f,k,G) is closed

let f be FinSequence of (TOP-REAL 2); :: thesis: for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

right_cell (f,k,G) is closed

let G be Go-board; :: thesis: ( 1 <= k & k + 1 <= len f & f is_sequence_on G implies right_cell (f,k,G) is closed )

assume A1: ( 1 <= k & k + 1 <= len f & f is_sequence_on G ) ; :: thesis: right_cell (f,k,G) is closed

then consider i1, j1, i2, j2 being Nat such that

A2: ( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) ) by JORDAN8:3;

( ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k,G) = cell (G,i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k,G) = cell (G,i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k,G) = cell (G,i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & right_cell (f,k,G) = cell (G,(i1 -' 1),j2) ) ) by A1, A2, Def1;

hence right_cell (f,k,G) is closed by GOBRD11:33; :: thesis: verum

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

right_cell (f,k,G) is closed

let f be FinSequence of (TOP-REAL 2); :: thesis: for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

right_cell (f,k,G) is closed

let G be Go-board; :: thesis: ( 1 <= k & k + 1 <= len f & f is_sequence_on G implies right_cell (f,k,G) is closed )

assume A1: ( 1 <= k & k + 1 <= len f & f is_sequence_on G ) ; :: thesis: right_cell (f,k,G) is closed

then consider i1, j1, i2, j2 being Nat such that

A2: ( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) ) by JORDAN8:3;

( ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k,G) = cell (G,i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k,G) = cell (G,i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k,G) = cell (G,i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & right_cell (f,k,G) = cell (G,(i1 -' 1),j2) ) ) by A1, A2, Def1;

hence right_cell (f,k,G) is closed by GOBRD11:33; :: thesis: verum