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 A10;

suppose A15: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: ex b₁ being Subset of st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b₁ = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell (GoB f),i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell (GoB f),(i1 -' 1),j2 )

take cell (GoB f),i1,j1 ; :: thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & cell (GoB f),i1,j1 = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & cell (GoB f),i1,j1 = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & cell (GoB f),i1,j1 = cell (GoB f),i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & cell (GoB f),i1,j1 = cell (GoB f),(i1 -' 1),j2 )
let i1', j1', i2', j2' be Element of NAT ; :: thesis: ( [i1',j1'] in Indices (GoB f) & [i2',j2'] in Indices (GoB f) & f /. k = (GoB f) * i1',j1' & f /. (k + 1) = (GoB f) * i2',j2' & not ( i1' = i2' & j1' + 1 = j2' & cell (GoB f),i1,j1 = cell (GoB f),i1',j1' ) & not ( i1' + 1 = i2' & j1' = j2' & cell (GoB f),i1,j1 = cell (GoB f),i1',(j1' -' 1) ) & not ( i1' = i2' + 1 & j1' = j2' & cell (GoB f),i1,j1 = cell (GoB f),i2',j2' ) implies ( i1' = i2' & j1' = j2' + 1 & cell (GoB f),i1,j1 = cell (GoB f),(i1' -' 1),j2' ) )
assume that
A16: [i1',j1'] in Indices (GoB f) and
A17: [i2',j2'] in Indices (GoB f) and
A18: f /. k = (GoB f) * i1',j1' and
A19: f /. (k + 1) = (GoB f) * i2',j2' ; :: thesis: ( ( i1' = i2' & j1' + 1 = j2' & cell (GoB f),i1,j1 = cell (GoB f),i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell (GoB f),i1,j1 = cell (GoB f),i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell (GoB f),i1,j1 = cell (GoB f),i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell (GoB f),i1,j1 = cell (GoB f),(i1' -' 1),j2' ) )
A20: i1 = i1' by A4, A5, A16, A18, GOBOARD1:21;
j1 = j1' by A4, A5, A16, A18, GOBOARD1:21;
hence ( ( i1' = i2' & j1' + 1 = j2' & cell (GoB f),i1,j1 = cell (GoB f),i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell (GoB f),i1,j1 = cell (GoB f),i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell (GoB f),i1,j1 = cell (GoB f),i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell (GoB f),i1,j1 = cell (GoB f),(i1' -' 1),j2' ) ) by A7, A8, A15, A17, A19, A20, GOBOARD1:21; :: thesis: verum

end;

suppose A21: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: ex b₁ being Subset of st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b₁ = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell (GoB f),i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell (GoB f),(i1 -' 1),j2 )

take cell (GoB f),i1,(j1 -' 1) ; :: thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),(i1 -' 1),j2 )
let i1', j1', i2', j2' be Element of NAT ; :: thesis: ( [i1',j1'] in Indices (GoB f) & [i2',j2'] in Indices (GoB f) & f /. k = (GoB f) * i1',j1' & f /. (k + 1) = (GoB f) * i2',j2' & not ( i1' = i2' & j1' + 1 = j2' & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),i1',j1' ) & not ( i1' + 1 = i2' & j1' = j2' & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),i1',(j1' -' 1) ) & not ( i1' = i2' + 1 & j1' = j2' & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),i2',j2' ) implies ( i1' = i2' & j1' = j2' + 1 & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),(i1' -' 1),j2' ) )
assume that
A22: [i1',j1'] in Indices (GoB f) and
A23: [i2',j2'] in Indices (GoB f) and
A24: f /. k = (GoB f) * i1',j1' and
A25: f /. (k + 1) = (GoB f) * i2',j2' ; :: thesis: ( ( i1' = i2' & j1' + 1 = j2' & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),(i1' -' 1),j2' ) )
A26: i1 = i1' by A4, A5, A22, A24, GOBOARD1:21;
j1 = j1' by A4, A5, A22, A24, GOBOARD1:21;
hence ( ( i1' = i2' & j1' + 1 = j2' & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell (GoB f),i1,(j1 -' 1) = cell (GoB f),(i1' -' 1),j2' ) ) by A7, A8, A21, A23, A25, A26, GOBOARD1:21; :: thesis: verum

end;

suppose A27: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: ex b₁ being Subset of st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b₁ = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell (GoB f),i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell (GoB f),(i1 -' 1),j2 )

take cell (GoB f),i2,j2 ; :: thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & cell (GoB f),i2,j2 = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & cell (GoB f),i2,j2 = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & cell (GoB f),i2,j2 = cell (GoB f),i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & cell (GoB f),i2,j2 = cell (GoB f),(i1 -' 1),j2 )
let i1', j1', i2', j2' be Element of NAT ; :: thesis: ( [i1',j1'] in Indices (GoB f) & [i2',j2'] in Indices (GoB f) & f /. k = (GoB f) * i1',j1' & f /. (k + 1) = (GoB f) * i2',j2' & not ( i1' = i2' & j1' + 1 = j2' & cell (GoB f),i2,j2 = cell (GoB f),i1',j1' ) & not ( i1' + 1 = i2' & j1' = j2' & cell (GoB f),i2,j2 = cell (GoB f),i1',(j1' -' 1) ) & not ( i1' = i2' + 1 & j1' = j2' & cell (GoB f),i2,j2 = cell (GoB f),i2',j2' ) implies ( i1' = i2' & j1' = j2' + 1 & cell (GoB f),i2,j2 = cell (GoB f),(i1' -' 1),j2' ) )
assume that
A28: [i1',j1'] in Indices (GoB f) and
A29: [i2',j2'] in Indices (GoB f) and
A30: f /. k = (GoB f) * i1',j1' and
A31: f /. (k + 1) = (GoB f) * i2',j2' ; :: thesis: ( ( i1' = i2' & j1' + 1 = j2' & cell (GoB f),i2,j2 = cell (GoB f),i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell (GoB f),i2,j2 = cell (GoB f),i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell (GoB f),i2,j2 = cell (GoB f),i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell (GoB f),i2,j2 = cell (GoB f),(i1' -' 1),j2' ) )
A32: i2 = i2' by A7, A8, A29, A31, GOBOARD1:21;
j1 = j1' by A4, A5, A28, A30, GOBOARD1:21;
hence ( ( i1' = i2' & j1' + 1 = j2' & cell (GoB f),i2,j2 = cell (GoB f),i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell (GoB f),i2,j2 = cell (GoB f),i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell (GoB f),i2,j2 = cell (GoB f),i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell (GoB f),i2,j2 = cell (GoB f),(i1' -' 1),j2' ) ) by A4, A5, A7, A8, A27, A28, A29, A30, A31, A32, GOBOARD1:21; :: thesis: verum

end;

suppose A33: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: ex b₁ being Subset of st
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b₁ = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell (GoB f),i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell (GoB f),(i1 -' 1),j2 )

take cell (GoB f),(i1 -' 1),j2 ; :: thesis: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),(i1 -' 1),j2 )
let i1', j1', i2', j2' be Element of NAT ; :: thesis: ( [i1',j1'] in Indices (GoB f) & [i2',j2'] in Indices (GoB f) & f /. k = (GoB f) * i1',j1' & f /. (k + 1) = (GoB f) * i2',j2' & not ( i1' = i2' & j1' + 1 = j2' & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),i1',j1' ) & not ( i1' + 1 = i2' & j1' = j2' & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),i1',(j1' -' 1) ) & not ( i1' = i2' + 1 & j1' = j2' & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),i2',j2' ) implies ( i1' = i2' & j1' = j2' + 1 & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),(i1' -' 1),j2' ) )
assume that
A34: [i1',j1'] in Indices (GoB f) and
A35: [i2',j2'] in Indices (GoB f) and
A36: f /. k = (GoB f) * i1',j1' and
A37: f /. (k + 1) = (GoB f) * i2',j2' ; :: thesis: ( ( i1' = i2' & j1' + 1 = j2' & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),(i1' -' 1),j2' ) )
A38: i1 = i1' by A4, A5, A34, A36, GOBOARD1:21;
j1 = j1' by A4, A5, A34, A36, GOBOARD1:21;
hence ( ( i1' = i2' & j1' + 1 = j2' & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell (GoB f),(i1 -' 1),j2 = cell (GoB f),(i1' -' 1),j2' ) ) by A7, A8, A33, A35, A37, A38, GOBOARD1:21; :: thesis: verum

end;

end;