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

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

take cell (G,(i2 -' 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,(i2 -' 1),j2) = cell (G,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & cell (G,(i2 -' 1),j2) = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & cell (G,(i2 -' 1),j2) = cell (G,(i2 -' 1),(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & cell (G,(i2 -' 1),j2) = cell (G,i2,(j2 -' 1)) )
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 -' 1),j2) = cell (G,(i29 -' 1),j29) ) & not ( i19 + 1 = i29 & j19 = j29 & cell (G,(i2 -' 1),j2) = cell (G,i29,j29) ) & not ( i19 = i29 + 1 & j19 = j29 & cell (G,(i2 -' 1),j2) = cell (G,(i29 -' 1),(j29 -' 1)) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (G,(i2 -' 1),j2) = cell (G,i29,(j29 -' 1)) ) )
assume A26: ( [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 -' 1),j2) = cell (G,(i29 -' 1),j29) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,(i2 -' 1),j2) = cell (G,i29,j29) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,(i2 -' 1),j2) = cell (G,(i29 -' 1),(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,(i2 -' 1),j2) = cell (G,i29,(j29 -' 1)) ) )
then ( i2 = i29 & j1 = j19 ) by A1, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell (G,(i2 -' 1),j2) = cell (G,(i29 -' 1),j29) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,(i2 -' 1),j2) = cell (G,i29,j29) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,(i2 -' 1),j2) = cell (G,(i29 -' 1),(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,(i2 -' 1),j2) = cell (G,i29,(j29 -' 1)) ) ) by A1, A25, A26, GOBOARD1:5; :: thesis: verum

end;

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

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,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & cell (G,i2,j2) = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & cell (G,i2,j2) = cell (G,(i2 -' 1),(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & cell (G,i2,j2) = cell (G,i2,(j2 -' 1)) )
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,(i29 -' 1),j29) ) & not ( i19 + 1 = i29 & j19 = j29 & cell (G,i2,j2) = cell (G,i29,j29) ) & not ( i19 = i29 + 1 & j19 = j29 & cell (G,i2,j2) = cell (G,(i29 -' 1),(j29 -' 1)) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (G,i2,j2) = cell (G,i29,(j29 -' 1)) ) )
assume A28: ( [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,(i29 -' 1),j29) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i2,j2) = cell (G,i29,j29) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i2,j2) = cell (G,(i29 -' 1),(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i2,j2) = cell (G,i29,(j29 -' 1)) ) )
then ( i2 = i29 & j1 = j19 ) by A1, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell (G,i2,j2) = cell (G,(i29 -' 1),j29) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i2,j2) = cell (G,i29,j29) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i2,j2) = cell (G,(i29 -' 1),(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i2,j2) = cell (G,i29,(j29 -' 1)) ) ) by A1, A27, A28, GOBOARD1:5; :: thesis: verum

end;

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

take cell (G,(i2 -' 1),(j2 -' 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,(i2 -' 1),(j2 -' 1)) = cell (G,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & cell (G,(i2 -' 1),(j2 -' 1)) = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & cell (G,(i2 -' 1),(j2 -' 1)) = cell (G,(i2 -' 1),(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & cell (G,(i2 -' 1),(j2 -' 1)) = cell (G,i2,(j2 -' 1)) )
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 -' 1),(j2 -' 1)) = cell (G,(i29 -' 1),j29) ) & not ( i19 + 1 = i29 & j19 = j29 & cell (G,(i2 -' 1),(j2 -' 1)) = cell (G,i29,j29) ) & not ( i19 = i29 + 1 & j19 = j29 & cell (G,(i2 -' 1),(j2 -' 1)) = cell (G,(i29 -' 1),(j29 -' 1)) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (G,(i2 -' 1),(j2 -' 1)) = cell (G,i29,(j29 -' 1)) ) )
assume A30: ( [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 -' 1),(j2 -' 1)) = cell (G,(i29 -' 1),j29) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,(i2 -' 1),(j2 -' 1)) = cell (G,i29,j29) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,(i2 -' 1),(j2 -' 1)) = cell (G,(i29 -' 1),(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,(i2 -' 1),(j2 -' 1)) = cell (G,i29,(j29 -' 1)) ) )
then ( i2 = i29 & j1 = j19 ) by A1, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell (G,(i2 -' 1),(j2 -' 1)) = cell (G,(i29 -' 1),j29) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,(i2 -' 1),(j2 -' 1)) = cell (G,i29,j29) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,(i2 -' 1),(j2 -' 1)) = cell (G,(i29 -' 1),(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,(i2 -' 1),(j2 -' 1)) = cell (G,i29,(j29 -' 1)) ) ) by A1, A29, A30, GOBOARD1:5; :: thesis: verum

end;

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

take cell (G,i2,(j2 -' 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,i2,(j2 -' 1)) = cell (G,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & cell (G,i2,(j2 -' 1)) = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & cell (G,i2,(j2 -' 1)) = cell (G,(i2 -' 1),(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & cell (G,i2,(j2 -' 1)) = cell (G,i2,(j2 -' 1)) )
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 -' 1)) = cell (G,(i29 -' 1),j29) ) & not ( i19 + 1 = i29 & j19 = j29 & cell (G,i2,(j2 -' 1)) = cell (G,i29,j29) ) & not ( i19 = i29 + 1 & j19 = j29 & cell (G,i2,(j2 -' 1)) = cell (G,(i29 -' 1),(j29 -' 1)) ) implies ( i19 = i29 & j19 = j29 + 1 & cell (G,i2,(j2 -' 1)) = cell (G,i29,(j29 -' 1)) ) )
assume A32: ( [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,(i29 -' 1),j29) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i2,(j2 -' 1)) = cell (G,i29,j29) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i2,(j2 -' 1)) = cell (G,(i29 -' 1),(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i2,(j2 -' 1)) = cell (G,i29,(j29 -' 1)) ) )
then ( i2 = i29 & j1 = j19 ) by A1, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell (G,i2,(j2 -' 1)) = cell (G,(i29 -' 1),j29) ) or ( i19 + 1 = i29 & j19 = j29 & cell (G,i2,(j2 -' 1)) = cell (G,i29,j29) ) or ( i19 = i29 + 1 & j19 = j29 & cell (G,i2,(j2 -' 1)) = cell (G,(i29 -' 1),(j29 -' 1)) ) or ( i19 = i29 & j19 = j29 + 1 & cell (G,i2,(j2 -' 1)) = cell (G,i29,(j29 -' 1)) ) ) by A1, A31, A32, GOBOARD1:5; :: thesis: verum

end;

end;