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 A49: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: ex b₁ being Subset of (TOP-REAL 2) 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 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell (GoB f),i1,j2 )

take cell (GoB f),(i1 -' 1),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 -' 1),j1 = cell (GoB f),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),i1,j2 )
let i19, j19, i29, j29 be Element of NAT ; :: thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * i19,j19 & f /. (k + 1) = (GoB f) * i29,j29 & not ( i19 = i29 & j19 + 1 = j29 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),(i19 -' 1),j19 ) & not ( i19 + 1 = i29 & j19 = j29 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),i19,j19 ) & not ( i19 = i29 + 1 & j19 = j29 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),i29,(j29 -' 1) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),i19,j29 ) )
assume that
A50: [i19,j19] in Indices (GoB f) and
A51: [i29,j29] in Indices (GoB f) and
A52: f /. k = (GoB f) * i19,j19 and
A53: f /. (k + 1) = (GoB f) * i29,j29 ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),i19,j29 ) )
A54: i1 = i19 by A4, A5, A50, A52, GOBOARD1:21;
j1 = j19 by A4, A5, A50, A52, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell (GoB f),(i1 -' 1),j1 = cell (GoB f),i19,j29 ) ) by A7, A8, A49, A51, A53, A54, GOBOARD1:21; :: thesis: verum

end;

suppose A55: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: ex b₁ being Subset of (TOP-REAL 2) 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 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell (GoB f),i1,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 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & cell (GoB f),i1,j1 = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & cell (GoB f),i1,j1 = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & cell (GoB f),i1,j1 = cell (GoB f),i1,j2 )
let i19, j19, i29, j29 be Element of NAT ; :: thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * i19,j19 & f /. (k + 1) = (GoB f) * i29,j29 & not ( i19 = i29 & j19 + 1 = j29 & cell (GoB f),i1,j1 = cell (GoB f),(i19 -' 1),j19 ) & not ( i19 + 1 = i29 & j19 = j29 & cell (GoB f),i1,j1 = cell (GoB f),i19,j19 ) & not ( i19 = i29 + 1 & j19 = j29 & cell (GoB f),i1,j1 = cell (GoB f),i29,(j29 -' 1) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (GoB f),i1,j1 = cell (GoB f),i19,j29 ) )
assume that
A56: [i19,j19] in Indices (GoB f) and
A57: [i29,j29] in Indices (GoB f) and
A58: f /. k = (GoB f) * i19,j19 and
A59: f /. (k + 1) = (GoB f) * i29,j29 ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell (GoB f),i1,j1 = cell (GoB f),(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell (GoB f),i1,j1 = cell (GoB f),i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell (GoB f),i1,j1 = cell (GoB f),i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell (GoB f),i1,j1 = cell (GoB f),i19,j29 ) )
A60: i1 = i19 by A4, A5, A56, A58, GOBOARD1:21;
j1 = j19 by A4, A5, A56, A58, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell (GoB f),i1,j1 = cell (GoB f),(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell (GoB f),i1,j1 = cell (GoB f),i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell (GoB f),i1,j1 = cell (GoB f),i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell (GoB f),i1,j1 = cell (GoB f),i19,j29 ) ) by A7, A8, A55, A57, A59, A60, GOBOARD1:21; :: thesis: verum

end;

suppose A61: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: ex b₁ being Subset of (TOP-REAL 2) 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 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell (GoB f),i1,j2 )

take cell (GoB f),i2,(j2 -' 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),i2,(j2 -' 1) = cell (GoB f),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),i1,j2 )
let i19, j19, i29, j29 be Element of NAT ; :: thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * i19,j19 & f /. (k + 1) = (GoB f) * i29,j29 & not ( i19 = i29 & j19 + 1 = j29 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),(i19 -' 1),j19 ) & not ( i19 + 1 = i29 & j19 = j29 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),i19,j19 ) & not ( i19 = i29 + 1 & j19 = j29 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),i29,(j29 -' 1) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),i19,j29 ) )
assume that
A62: [i19,j19] in Indices (GoB f) and
A63: [i29,j29] in Indices (GoB f) and
A64: f /. k = (GoB f) * i19,j19 and
A65: f /. (k + 1) = (GoB f) * i29,j29 ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),i19,j29 ) )
A66: i2 = i29 by A7, A8, A63, A65, GOBOARD1:21;
j1 = j19 by A4, A5, A62, A64, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell (GoB f),i2,(j2 -' 1) = cell (GoB f),i19,j29 ) ) by A4, A5, A7, A8, A61, A62, A63, A64, A65, A66, GOBOARD1:21; :: thesis: verum

end;

suppose A67: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: ex b₁ being Subset of (TOP-REAL 2) 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 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell (GoB f),i1,j2 )

take cell (GoB f),i1,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,j2 = cell (GoB f),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & cell (GoB f),i1,j2 = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & cell (GoB f),i1,j2 = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & cell (GoB f),i1,j2 = cell (GoB f),i1,j2 )
let i19, j19, i29, j29 be Element of NAT ; :: thesis: ( [i19,j19] in Indices (GoB f) & [i29,j29] in Indices (GoB f) & f /. k = (GoB f) * i19,j19 & f /. (k + 1) = (GoB f) * i29,j29 & not ( i19 = i29 & j19 + 1 = j29 & cell (GoB f),i1,j2 = cell (GoB f),(i19 -' 1),j19 ) & not ( i19 + 1 = i29 & j19 = j29 & cell (GoB f),i1,j2 = cell (GoB f),i19,j19 ) & not ( i19 = i29 + 1 & j19 = j29 & cell (GoB f),i1,j2 = cell (GoB f),i29,(j29 -' 1) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (GoB f),i1,j2 = cell (GoB f),i19,j29 ) )
assume that
A68: [i19,j19] in Indices (GoB f) and
A69: [i29,j29] in Indices (GoB f) and
A70: f /. k = (GoB f) * i19,j19 and
A71: f /. (k + 1) = (GoB f) * i29,j29 ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell (GoB f),i1,j2 = cell (GoB f),(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell (GoB f),i1,j2 = cell (GoB f),i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell (GoB f),i1,j2 = cell (GoB f),i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell (GoB f),i1,j2 = cell (GoB f),i19,j29 ) )
A72: i1 = i19 by A4, A5, A68, A70, GOBOARD1:21;
j1 = j19 by A4, A5, A68, A70, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell (GoB f),i1,j2 = cell (GoB f),(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell (GoB f),i1,j2 = cell (GoB f),i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell (GoB f),i1,j2 = cell (GoB f),i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell (GoB f),i1,j2 = cell (GoB f),i19,j29 ) ) by A7, A8, A67, A69, A71, A72, GOBOARD1:21; :: thesis: verum

end;

end;