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

suppose A6: ( 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,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell G,i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell G,i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell G,(i1 -' 1),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,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 i1', j1', i2', j2' be Element of NAT ; :: thesis: ( [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' ) implies ( i1' = i2' & j1' = j2' + 1 & cell G,i1,j1 = cell G,(i1' -' 1),j2' ) )
assume ( [i1',j1'] in Indices G & [i2',j2'] in Indices G & f /. k = G * i1',j1' & f /. (k + 1) = G * i2',j2' ) ; :: thesis: ( ( i1' = i2' & j1' + 1 = j2' & cell G,i1,j1 = cell G,i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell G,i1,j1 = cell G,i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell G,i1,j1 = cell G,i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell G,i1,j1 = cell G,(i1' -' 1),j2' ) )
then ( i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' ) by A3, A4, GOBOARD1:21;
hence ( ( i1' = i2' & j1' + 1 = j2' & cell G,i1,j1 = cell G,i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell G,i1,j1 = cell G,i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell G,i1,j1 = cell G,i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell G,i1,j1 = cell G,(i1' -' 1),j2' ) ) by A6; :: thesis: verum

end;

suppose A7: ( 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,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell G,i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell G,i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell G,(i1 -' 1),j2 )

take cell G,i1,(j1 -' 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,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 i1', j1', i2', j2' be Element of NAT ; :: thesis: ( [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' ) implies ( i1' = i2' & j1' = j2' + 1 & cell G,i1,(j1 -' 1) = cell G,(i1' -' 1),j2' ) )
assume ( [i1',j1'] in Indices G & [i2',j2'] in Indices G & f /. k = G * i1',j1' & f /. (k + 1) = G * i2',j2' ) ; :: thesis: ( ( i1' = i2' & j1' + 1 = j2' & cell G,i1,(j1 -' 1) = cell G,i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell G,i1,(j1 -' 1) = cell G,i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell G,i1,(j1 -' 1) = cell G,i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell G,i1,(j1 -' 1) = cell G,(i1' -' 1),j2' ) )
then ( i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' ) by A3, A4, GOBOARD1:21;
hence ( ( i1' = i2' & j1' + 1 = j2' & cell G,i1,(j1 -' 1) = cell G,i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell G,i1,(j1 -' 1) = cell G,i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell G,i1,(j1 -' 1) = cell G,i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell G,i1,(j1 -' 1) = cell G,(i1' -' 1),j2' ) ) by A7; :: thesis: verum

end;

suppose A8: ( 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,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell G,i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell G,i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell G,(i1 -' 1),j2 )

take cell G,i2,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,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 i1', j1', i2', j2' be Element of NAT ; :: thesis: ( [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' ) implies ( i1' = i2' & j1' = j2' + 1 & cell G,i2,j2 = cell G,(i1' -' 1),j2' ) )
assume ( [i1',j1'] in Indices G & [i2',j2'] in Indices G & f /. k = G * i1',j1' & f /. (k + 1) = G * i2',j2' ) ; :: thesis: ( ( i1' = i2' & j1' + 1 = j2' & cell G,i2,j2 = cell G,i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell G,i2,j2 = cell G,i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell G,i2,j2 = cell G,i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell G,i2,j2 = cell G,(i1' -' 1),j2' ) )
then ( i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' ) by A3, A4, GOBOARD1:21;
hence ( ( i1' = i2' & j1' + 1 = j2' & cell G,i2,j2 = cell G,i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell G,i2,j2 = cell G,i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell G,i2,j2 = cell G,i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell G,i2,j2 = cell G,(i1' -' 1),j2' ) ) by A8; :: thesis: verum

end;

suppose A9: ( 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,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & b₁ = cell G,i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & b₁ = cell G,i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & b₁ = cell G,(i1 -' 1),j2 )

take cell G,(i1 -' 1),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 -' 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 i1', j1', i2', j2' be Element of NAT ; :: thesis: ( [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' ) implies ( i1' = i2' & j1' = j2' + 1 & cell G,(i1 -' 1),j2 = cell G,(i1' -' 1),j2' ) )
assume ( [i1',j1'] in Indices G & [i2',j2'] in Indices G & f /. k = G * i1',j1' & f /. (k + 1) = G * i2',j2' ) ; :: thesis: ( ( i1' = i2' & j1' + 1 = j2' & cell G,(i1 -' 1),j2 = cell G,i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell G,(i1 -' 1),j2 = cell G,i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell G,(i1 -' 1),j2 = cell G,i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell G,(i1 -' 1),j2 = cell G,(i1' -' 1),j2' ) )
then ( i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' ) by A3, A4, GOBOARD1:21;
hence ( ( i1' = i2' & j1' + 1 = j2' & cell G,(i1 -' 1),j2 = cell G,i1',j1' ) or ( i1' + 1 = i2' & j1' = j2' & cell G,(i1 -' 1),j2 = cell G,i1',(j1' -' 1) ) or ( i1' = i2' + 1 & j1' = j2' & cell G,(i1 -' 1),j2 = cell G,i2',j2' ) or ( i1' = i2' & j1' = j2' + 1 & cell G,(i1 -' 1),j2 = cell G,(i1' -' 1),j2' ) ) by A9; :: thesis: verum

end;

end;