for m, n being Nat
for K being Field
for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )