theorem Th3: :: GOBOARD1:4

for M being Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2)
for x being set
for n, m being Nat st x in rng (Col (M,n)) & x in rng (Col (M,m)) & n in Seg (width M) & m in Seg (width M) holds
n = m