per cases
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A3;

end;

suppose A4:
( i1 = i2 & j1 + 1 = j2 )
; :: thesis: ex b_{1} being Subset of (TOP-REAL 2) st

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{1} = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell (G,i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell (G,(i1 -' 1),j2) )

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b

( i1 = i2 & j1 = j2 + 1 & b

take
cell (G,i1,j1)
; :: thesis: for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell (G,i1,j1) = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell (G,i1,j1) = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell (G,i1,j1) = cell (G,i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & cell (G,i1,j1) = cell (G,(i1 -' 1),j2) )

let i19, j19, i29, j29 be Nat; :: thesis: ( [i19,j19] in Indices G & [i29,j29] in Indices G & f /. k = G * (i19,j19) & f /. (k + 1) = G * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell (G,i1,j1) = cell (G,i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell (G,i1,j1) = cell (G,i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell (G,i1,j1) = cell (G,i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (G,i1,j1) = cell (G,(i19 -' 1),j29) ) )

assume that

A5: [i19,j19] in Indices G and

A6: [i29,j29] in Indices G and

A7: f /. k = G * (i19,j19) and

A8: f /. (k + 1) = G * (i29,j29) ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell (G,i1,j1) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i1,j1) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i1,j1) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i1,j1) = cell (G,(i19 -' 1),j29) ) )

( i1 = i19 & j1 = j19 ) by A1, A5, A7, GOBOARD1:5;

hence ( ( i19 = i29 & j19 + 1 = j29 & cell (G,i1,j1) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i1,j1) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i1,j1) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i1,j1) = cell (G,(i19 -' 1),j29) ) ) by A2, A4, A6, A8, GOBOARD1:5; :: thesis: verum

end;( i1 = i2 & j1 = j2 + 1 & cell (G,i1,j1) = cell (G,(i1 -' 1),j2) )

let i19, j19, i29, j29 be Nat; :: thesis: ( [i19,j19] in Indices G & [i29,j29] in Indices G & f /. k = G * (i19,j19) & f /. (k + 1) = G * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell (G,i1,j1) = cell (G,i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell (G,i1,j1) = cell (G,i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell (G,i1,j1) = cell (G,i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (G,i1,j1) = cell (G,(i19 -' 1),j29) ) )

assume that

A5: [i19,j19] in Indices G and

A6: [i29,j29] in Indices G and

A7: f /. k = G * (i19,j19) and

A8: f /. (k + 1) = G * (i29,j29) ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell (G,i1,j1) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i1,j1) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i1,j1) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i1,j1) = cell (G,(i19 -' 1),j29) ) )

( i1 = i19 & j1 = j19 ) by A1, A5, A7, GOBOARD1:5;

hence ( ( i19 = i29 & j19 + 1 = j29 & cell (G,i1,j1) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i1,j1) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i1,j1) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i1,j1) = cell (G,(i19 -' 1),j29) ) ) by A2, A4, A6, A8, GOBOARD1:5; :: thesis: verum

suppose A9:
( i1 + 1 = i2 & j1 = j2 )
; :: thesis: ex b_{1} being Subset of (TOP-REAL 2) st

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{1} = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell (G,i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell (G,(i1 -' 1),j2) )

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b

( i1 = i2 & j1 = j2 + 1 & b

take
cell (G,i1,(j1 -' 1))
; :: thesis: for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell (G,i1,(j1 -' 1)) = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell (G,i1,(j1 -' 1)) = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell (G,i1,(j1 -' 1)) = cell (G,i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & cell (G,i1,(j1 -' 1)) = cell (G,(i1 -' 1),j2) )

let i19, j19, i29, j29 be Nat; :: thesis: ( [i19,j19] in Indices G & [i29,j29] in Indices G & f /. k = G * (i19,j19) & f /. (k + 1) = G * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (G,i1,(j1 -' 1)) = cell (G,(i19 -' 1),j29) ) )

assume that

A10: [i19,j19] in Indices G and

A11: [i29,j29] in Indices G and

A12: f /. k = G * (i19,j19) and

A13: f /. (k + 1) = G * (i29,j29) ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i1,(j1 -' 1)) = cell (G,(i19 -' 1),j29) ) )

( i1 = i19 & j1 = j19 ) by A1, A10, A12, GOBOARD1:5;

hence ( ( i19 = i29 & j19 + 1 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i1,(j1 -' 1)) = cell (G,(i19 -' 1),j29) ) ) by A2, A9, A11, A13, GOBOARD1:5; :: thesis: verum

end;( i1 = i2 & j1 = j2 + 1 & cell (G,i1,(j1 -' 1)) = cell (G,(i1 -' 1),j2) )

let i19, j19, i29, j29 be Nat; :: thesis: ( [i19,j19] in Indices G & [i29,j29] in Indices G & f /. k = G * (i19,j19) & f /. (k + 1) = G * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (G,i1,(j1 -' 1)) = cell (G,(i19 -' 1),j29) ) )

assume that

A10: [i19,j19] in Indices G and

A11: [i29,j29] in Indices G and

A12: f /. k = G * (i19,j19) and

A13: f /. (k + 1) = G * (i29,j29) ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i1,(j1 -' 1)) = cell (G,(i19 -' 1),j29) ) )

( i1 = i19 & j1 = j19 ) by A1, A10, A12, GOBOARD1:5;

hence ( ( i19 = i29 & j19 + 1 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i1,(j1 -' 1)) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i1,(j1 -' 1)) = cell (G,(i19 -' 1),j29) ) ) by A2, A9, A11, A13, GOBOARD1:5; :: thesis: verum

suppose A14:
( i1 = i2 + 1 & j1 = j2 )
; :: thesis: ex b_{1} being Subset of (TOP-REAL 2) st

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{1} = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell (G,i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell (G,(i1 -' 1),j2) )

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b

( i1 = i2 & j1 = j2 + 1 & b

take
cell (G,i2,j2)
; :: thesis: for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell (G,i2,j2) = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell (G,i2,j2) = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell (G,i2,j2) = cell (G,i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & cell (G,i2,j2) = cell (G,(i1 -' 1),j2) )

let i19, j19, i29, j29 be Nat; :: thesis: ( [i19,j19] in Indices G & [i29,j29] in Indices G & f /. k = G * (i19,j19) & f /. (k + 1) = G * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell (G,i2,j2) = cell (G,i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell (G,i2,j2) = cell (G,i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell (G,i2,j2) = cell (G,i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (G,i2,j2) = cell (G,(i19 -' 1),j29) ) )

assume A15: ( [i19,j19] in Indices G & [i29,j29] in Indices G & f /. k = G * (i19,j19) & f /. (k + 1) = G * (i29,j29) ) ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell (G,i2,j2) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i2,j2) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i2,j2) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i2,j2) = cell (G,(i19 -' 1),j29) ) )

then ( i2 = i29 & j1 = j19 ) by A1, A2, GOBOARD1:5;

hence ( ( i19 = i29 & j19 + 1 = j29 & cell (G,i2,j2) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i2,j2) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i2,j2) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i2,j2) = cell (G,(i19 -' 1),j29) ) ) by A1, A2, A14, A15, GOBOARD1:5; :: thesis: verum

end;( i1 = i2 & j1 = j2 + 1 & cell (G,i2,j2) = cell (G,(i1 -' 1),j2) )

let i19, j19, i29, j29 be Nat; :: thesis: ( [i19,j19] in Indices G & [i29,j29] in Indices G & f /. k = G * (i19,j19) & f /. (k + 1) = G * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell (G,i2,j2) = cell (G,i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell (G,i2,j2) = cell (G,i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell (G,i2,j2) = cell (G,i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (G,i2,j2) = cell (G,(i19 -' 1),j29) ) )

assume A15: ( [i19,j19] in Indices G & [i29,j29] in Indices G & f /. k = G * (i19,j19) & f /. (k + 1) = G * (i29,j29) ) ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell (G,i2,j2) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i2,j2) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i2,j2) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i2,j2) = cell (G,(i19 -' 1),j29) ) )

then ( i2 = i29 & j1 = j19 ) by A1, A2, GOBOARD1:5;

hence ( ( i19 = i29 & j19 + 1 = j29 & cell (G,i2,j2) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i2,j2) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i2,j2) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i2,j2) = cell (G,(i19 -' 1),j29) ) ) by A1, A2, A14, A15, GOBOARD1:5; :: thesis: verum

suppose A16:
( i1 = i2 & j1 = j2 + 1 )
; :: thesis: ex b_{1} being Subset of (TOP-REAL 2) st

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{1} = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell (G,i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell (G,(i1 -' 1),j2) )

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b

( i1 = i2 & j1 = j2 + 1 & b

take
cell (G,(i1 -' 1),j2)
; :: thesis: for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell (G,(i1 -' 1),j2) = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell (G,(i1 -' 1),j2) = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell (G,(i1 -' 1),j2) = cell (G,i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & cell (G,(i1 -' 1),j2) = cell (G,(i1 -' 1),j2) )

let i19, j19, i29, j29 be Nat; :: thesis: ( [i19,j19] in Indices G & [i29,j29] in Indices G & f /. k = G * (i19,j19) & f /. (k + 1) = G * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (G,(i1 -' 1),j2) = cell (G,(i19 -' 1),j29) ) )

assume that

A17: [i19,j19] in Indices G and

A18: [i29,j29] in Indices G and

A19: f /. k = G * (i19,j19) and

A20: f /. (k + 1) = G * (i29,j29) ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,(i1 -' 1),j2) = cell (G,(i19 -' 1),j29) ) )

( i1 = i19 & j1 = j19 ) by A1, A17, A19, GOBOARD1:5;

hence ( ( i19 = i29 & j19 + 1 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,(i1 -' 1),j2) = cell (G,(i19 -' 1),j29) ) ) by A2, A16, A18, A20, GOBOARD1:5; :: thesis: verum

end;( i1 = i2 & j1 = j2 + 1 & cell (G,(i1 -' 1),j2) = cell (G,(i1 -' 1),j2) )

let i19, j19, i29, j29 be Nat; :: thesis: ( [i19,j19] in Indices G & [i29,j29] in Indices G & f /. k = G * (i19,j19) & f /. (k + 1) = G * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i19,j19) ) & not ( i19 + 1 = i29 & j19 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i19,(j19 -' 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i29,j29) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (G,(i1 -' 1),j2) = cell (G,(i19 -' 1),j29) ) )

assume that

A17: [i19,j19] in Indices G and

A18: [i29,j29] in Indices G and

A19: f /. k = G * (i19,j19) and

A20: f /. (k + 1) = G * (i29,j29) ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,(i1 -' 1),j2) = cell (G,(i19 -' 1),j29) ) )

( i1 = i19 & j1 = j19 ) by A1, A17, A19, GOBOARD1:5;

hence ( ( i19 = i29 & j19 + 1 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,(i1 -' 1),j2) = cell (G,i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,(i1 -' 1),j2) = cell (G,(i19 -' 1),j29) ) ) by A2, A16, A18, A20, GOBOARD1:5; :: thesis: verum