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,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 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 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 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

( i1 = i2 & j1 = j2 + 1 & P1 = cell (G,(i2 -' 1),(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,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 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 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;

end;

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:29;

hence P1 = cell (G,i2,j2) by A1, A11, A14

.= P2 by A1, A12, A15, A14 ;

:: thesis: verum

end;A15: j1 < j2 by A13, XREAL_1:29;

hence P1 = cell (G,i2,j2) by A1, A11, A14

.= P2 by A1, A12, A15, A14 ;

:: thesis: verum

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:29;

hence P1 = cell (G,i2,(j2 -' 1)) by A1, A11, A17

.= P2 by A1, A12, A18, A17 ;

:: thesis: verum

end;A18: i1 < i2 by A16, XREAL_1:29;

hence P1 = cell (G,i2,(j2 -' 1)) by A1, A11, A17

.= P2 by A1, A12, A18, A17 ;

:: thesis: verum