let P1, P2 be Subset of (TOP-REAL 2); :: thesis: ( ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & P1 = cell (GoB f),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & P1 = cell (GoB f),i1,j2 ) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & P2 = cell (GoB f),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & P2 = cell (GoB f),i1,j2 ) ) implies P1 = P2 )
assume that
A30: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & P1 = cell (GoB f),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & P1 = cell (GoB f),i1,j2 ) and
A31: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & P2 = cell (GoB f),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell (GoB f),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell (GoB f),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & P2 = cell (GoB f),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 A7;

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

then A32: j1 < j2 by XREAL_1:31;
A33: j2 <= j2 + 1 by NAT_1:11;
hence P1 = cell (GoB f),(i1 -' 1),j1 by A3, A5, A30, A32
.= P2 by A3, A5, A31, A32, A33 ;
:: thesis: verum

end;

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

then A34: i1 < i2 by XREAL_1:31;
A35: i2 <= i2 + 1 by NAT_1:11;
hence P1 = cell (GoB f),i1,j1 by A3, A5, A30, A34
.= P2 by A3, A5, A31, A34, A35 ;
:: thesis: verum

end;

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

then A36: i2 < i1 by XREAL_1:31;
A37: i1 <= i1 + 1 by NAT_1:11;
hence P1 = cell (GoB f),i2,(j2 -' 1) by A3, A5, A30, A36
.= P2 by A3, A5, A31, A36, A37 ;
:: thesis: verum

end;

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

then A38: j2 < j1 by XREAL_1:31;
A39: j1 <= j1 + 1 by NAT_1:11;
hence P1 = cell (GoB f),i1,j2 by A3, A5, A30, A38
.= P2 by A3, A5, A31, A38, A39 ;
:: thesis: verum

end;

end;