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

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

A14: j2 <= j2 + 1 by NAT_1:11;
A15: j1 < j2 by A13, XREAL_1:31;
hence P1 = cell G,i2,j2 by A1, A11, A14
.= P2 by A1, A12, A15, A14 ;
:: thesis: verum

end;

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

A17: i2 <= i2 + 1 by NAT_1:11;
A18: i1 < i2 by A16, XREAL_1:31;
hence P1 = cell G,i2,(j2 -' 1) by A1, A11, A17
.= P2 by A1, A12, A18, A17 ;
:: thesis: verum

end;

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

A20: i1 <= i1 + 1 by NAT_1:11;
A21: i2 < i1 by A19, XREAL_1:31;
hence P1 = cell G,(i2 -' 1),j2 by A1, A11, A20
.= P2 by A1, A12, A21, A20 ;
:: thesis: verum

end;

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

A23: j1 <= j1 + 1 by NAT_1:11;
A24: j2 < j1 by A22, XREAL_1:31;
hence P1 = cell G,(i2 -' 1),(j2 -' 1) by A1, A11, A23
.= P2 by A1, A12, A24, A23 ;
:: thesis: verum

end;

end;