theorem Th80: :: MATRIX13:80

for K being Field
for M being Matrix of K
for P, P1, Q, Q1 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 holds
the_rank_of (Segm (M,P,Q)) <= the_rank_of (Segm (M,P1,Q1))