theorem :: MATRTOP2:13

for n, m being Nat
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
M is OrdBasis of Lin (lines M)