theorem Th2: :: GOBOARD1:3

for M being X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2)
for x being set
for n, m being Nat st x in rng (Line (M,n)) & x in rng (Line (M,m)) & n in dom M & m in dom M holds
n = m