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;

suppose A35: ( 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 G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b₁ = cell G,(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell G,i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell G,i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell G,i1,j2 )

take cell G,(i1 -' 1),j1 ; :: thesis: for i1, j1, i2, j2 being Element of 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),j1 = cell G,(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & cell G,(i1 -' 1),j1 = cell G,i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & cell G,(i1 -' 1),j1 = cell G,i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & cell G,(i1 -' 1),j1 = cell G,i1,j2 )
let i19, j19, i29, j29 be Element of 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),j1 = cell G,(i19 -' 1),j19 ) & not ( i19 + 1 = i29 & j19 = j29 & cell G,(i1 -' 1),j1 = cell G,i19,j19 ) & not ( i19 = i29 + 1 & j19 = j29 & cell G,(i1 -' 1),j1 = cell G,i29,(j29 -' 1) ) implies ( i19 = i29 & j19 = j29 + 1 & cell G,(i1 -' 1),j1 = cell G,i19,j29 ) )
assume that
A36: [i19,j19] in Indices G and
A37: [i29,j29] in Indices G and
A38: f /. k = G * i19,j19 and
A39: f /. (k + 1) = G * i29,j29 ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell G,(i1 -' 1),j1 = cell G,(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell G,(i1 -' 1),j1 = cell G,i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell G,(i1 -' 1),j1 = cell G,i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell G,(i1 -' 1),j1 = cell G,i19,j29 ) )
( i1 = i19 & j1 = j19 ) by A1, A36, A38, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell G,(i1 -' 1),j1 = cell G,(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell G,(i1 -' 1),j1 = cell G,i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell G,(i1 -' 1),j1 = cell G,i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell G,(i1 -' 1),j1 = cell G,i19,j29 ) ) by A2, A35, A37, A39, GOBOARD1:21; :: thesis: verum

end;

suppose A40: ( 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 G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b₁ = cell G,(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell G,i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell G,i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell G,i1,j2 )

take cell G,i1,j1 ; :: thesis: for i1, j1, i2, j2 being Element of 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 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & cell G,i1,j1 = cell G,i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & cell G,i1,j1 = cell G,i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & cell G,i1,j1 = cell G,i1,j2 )
let i19, j19, i29, j29 be Element of 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 -' 1),j19 ) & not ( i19 + 1 = i29 & j19 = j29 & cell G,i1,j1 = cell G,i19,j19 ) & not ( i19 = i29 + 1 & j19 = j29 & cell G,i1,j1 = cell G,i29,(j29 -' 1) ) implies ( i19 = i29 & j19 = j29 + 1 & cell G,i1,j1 = cell G,i19,j29 ) )
assume that
A41: [i19,j19] in Indices G and
A42: [i29,j29] in Indices G and
A43: f /. k = G * i19,j19 and
A44: f /. (k + 1) = G * i29,j29 ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell G,i1,j1 = cell G,(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell G,i1,j1 = cell G,i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell G,i1,j1 = cell G,i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell G,i1,j1 = cell G,i19,j29 ) )
( i1 = i19 & j1 = j19 ) by A1, A41, A43, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell G,i1,j1 = cell G,(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell G,i1,j1 = cell G,i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell G,i1,j1 = cell G,i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell G,i1,j1 = cell G,i19,j29 ) ) by A2, A40, A42, A44, GOBOARD1:21; :: thesis: verum

end;

suppose A45: ( 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 G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b₁ = cell G,(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell G,i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell G,i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell G,i1,j2 )

take cell G,i2,(j2 -' 1) ; :: thesis: for i1, j1, i2, j2 being Element of 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 -' 1) = cell G,(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & cell G,i2,(j2 -' 1) = cell G,i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & cell G,i2,(j2 -' 1) = cell G,i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & cell G,i2,(j2 -' 1) = cell G,i1,j2 )
let i19, j19, i29, j29 be Element of 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 -' 1) = cell G,(i19 -' 1),j19 ) & not ( i19 + 1 = i29 & j19 = j29 & cell G,i2,(j2 -' 1) = cell G,i19,j19 ) & not ( i19 = i29 + 1 & j19 = j29 & cell G,i2,(j2 -' 1) = cell G,i29,(j29 -' 1) ) implies ( i19 = i29 & j19 = j29 + 1 & cell G,i2,(j2 -' 1) = cell G,i19,j29 ) )
assume A46: ( [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 -' 1) = cell G,(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell G,i2,(j2 -' 1) = cell G,i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell G,i2,(j2 -' 1) = cell G,i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell G,i2,(j2 -' 1) = cell G,i19,j29 ) )
then ( i2 = i29 & j1 = j19 ) by A1, A2, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell G,i2,(j2 -' 1) = cell G,(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell G,i2,(j2 -' 1) = cell G,i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell G,i2,(j2 -' 1) = cell G,i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell G,i2,(j2 -' 1) = cell G,i19,j29 ) ) by A1, A2, A45, A46, GOBOARD1:21; :: thesis: verum

end;

suppose A47: ( 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 G & [i2,j2] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & b₁ = cell G,(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell G,i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell G,i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell G,i1,j2 )

take cell G,i1,j2 ; :: thesis: for i1, j1, i2, j2 being Element of 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,j2 = cell G,(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & cell G,i1,j2 = cell G,i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & cell G,i1,j2 = cell G,i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & cell G,i1,j2 = cell G,i1,j2 )
let i19, j19, i29, j29 be Element of 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,j2 = cell G,(i19 -' 1),j19 ) & not ( i19 + 1 = i29 & j19 = j29 & cell G,i1,j2 = cell G,i19,j19 ) & not ( i19 = i29 + 1 & j19 = j29 & cell G,i1,j2 = cell G,i29,(j29 -' 1) ) implies ( i19 = i29 & j19 = j29 + 1 & cell G,i1,j2 = cell G,i19,j29 ) )
assume that
A48: [i19,j19] in Indices G and
A49: [i29,j29] in Indices G and
A50: f /. k = G * i19,j19 and
A51: f /. (k + 1) = G * i29,j29 ; :: thesis: ( ( i19 = i29 & j19 + 1 = j29 & cell G,i1,j2 = cell G,(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell G,i1,j2 = cell G,i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell G,i1,j2 = cell G,i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell G,i1,j2 = cell G,i19,j29 ) )
( i1 = i19 & j1 = j19 ) by A1, A48, A50, GOBOARD1:21;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell G,i1,j2 = cell G,(i19 -' 1),j19 ) or ( i19 + 1 = i29 & j19 = j29 & cell G,i1,j2 = cell G,i19,j19 ) or ( i19 = i29 + 1 & j19 = j29 & cell G,i1,j2 = cell G,i29,(j29 -' 1) ) or ( i19 = i29 & j19 = j29 + 1 & cell G,i1,j2 = cell G,i19,j29 ) ) by A2, A47, A49, A51, GOBOARD1:21; :: thesis: verum

end;

end;