theorem Th7: :: JORDAN1G:7

for G being X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2)
for i1, i2, j1, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & (G * (i1,j1)) `1 = (G * (i2,j2)) `1 holds
i1 = i2