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,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell (G,(i2 -' 1),(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & P1 = cell (G,i2,(j2 -' 1)) ) ) & ( 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,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell (G,(i2 -' 1),(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & P2 = cell (G,i2,(j2 -' 1)) ) ) implies P1 = P2 )
assume that
A33: 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,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell (G,(i2 -' 1),(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & P1 = cell (G,i2,(j2 -' 1)) ) and
A34: 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,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell (G,(i2 -' 1),(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & P2 = cell (G,i2,(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 A35: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: P1 = P2
A36: j2 <= j2 + 1 by NAT_1:11;
A37: j1 < j2 by A35, XREAL_1:29;
hence P1 = cell (G,(i2 -' 1),j2) by A1, A33, A36
.= P2 by A1, A34, A37, A36 ;
:: thesis: verum
end;
suppose A38: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: P1 = P2
A39: i2 <= i2 + 1 by NAT_1:11;
A40: i1 < i2 by A38, XREAL_1:29;
hence P1 = cell (G,i2,j2) by A1, A33, A39
.= P2 by A1, A34, A40, A39 ;
:: thesis: verum
end;
suppose A41: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: P1 = P2
A42: i1 <= i1 + 1 by NAT_1:11;
A43: i2 < i1 by A41, XREAL_1:29;
hence P1 = cell (G,(i2 -' 1),(j2 -' 1)) by A1, A33, A42
.= P2 by A1, A34, A43, A42 ;
:: thesis: verum
end;
suppose A44: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: P1 = P2
A45: j1 <= j1 + 1 by NAT_1:11;
A46: j2 < j1 by A44, XREAL_1:29;
hence P1 = cell (G,i2,(j2 -' 1)) by A1, A33, A45
.= P2 by A1, A34, A46, A45 ;
:: thesis: verum
end;
end;