theorem Th43: :: MATRIX13:43

for N being finite without_zero Subset of NAT ex k being Nat st N c= Seg k