let K be Field; :: thesis: for M being Matrix of K holds
( the_rank_of M <= len M & the_rank_of M <= width M )
let M be Matrix of K; :: thesis: ( the_rank_of M <= len M & the_rank_of M <= width M )
ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = the_rank_of M & Det (EqSegm (M,P,Q)) <> 0. K ) by Def4;
hence ( the_rank_of M <= len M & the_rank_of M <= width M ) by Th73; :: thesis: verum