for x being object
for m, n being Nat
for K being Field
for M being Matrix of m,n,K holds
( x in lines M iff ex i being Nat st
( i in Seg m & x = Line (M,i) ) )