let P1, P2 be Subset of (TOP-REAL 2); :: 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 & P1 = cell (G,(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell (G,i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell (G,i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & P1 = cell (G,i1,j2) ) ) & ( 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 & P2 = cell (G,(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell (G,i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell (G,i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & P2 = cell (G,i1,j2) ) ) implies P1 = P2 )
assume that
A52: 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 & P1 = cell (G,(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell (G,i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell (G,i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & P1 = cell (G,i1,j2) ) and
A53: 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 & P2 = cell (G,(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell (G,i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell (G,i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & P2 = cell (G,i1,j2) ) ; :: thesis: P1 = P2

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 A54: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: P1 = P2

A55: j2 <= j2 + 1 by NAT_1:11;
A56: j1 < j2 by A54, XREAL_1:29;
hence P1 = cell (G,(i1 -' 1),j1) by A1, A2, A52, A55
.= P2 by A1, A2, A53, A56, A55 ;
:: thesis: verum

end;

suppose A57: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: P1 = P2

A58: i2 <= i2 + 1 by NAT_1:11;
A59: i1 < i2 by A57, XREAL_1:29;
hence P1 = cell (G,i1,j1) by A1, A2, A52, A58
.= P2 by A1, A2, A53, A59, A58 ;
:: thesis: verum

end;

suppose A60: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: P1 = P2

A61: i1 <= i1 + 1 by NAT_1:11;
A62: i2 < i1 by A60, XREAL_1:29;
hence P1 = cell (G,i2,(j2 -' 1)) by A1, A2, A52, A61
.= P2 by A1, A2, A53, A62, A61 ;
:: thesis: verum

end;

suppose A63: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: P1 = P2

A64: j1 <= j1 + 1 by NAT_1:11;
A65: j2 < j1 by A63, XREAL_1:29;
hence P1 = cell (G,i1,j2) by A1, A2, A52, A64
.= P2 by A1, A2, A53, A65, A64 ;
:: thesis: verum

end;

end;