theorem Th31: :: ANPROJ_8:37

for k being Nat
for M being Matrix of k,F_Real holds
( ( lines M is linearly-dependent or not M is without_repeated_line ) iff the_rank_of M < k )