theorem Th43: :: MATRIX13:43

for N being finite without_zero Subset of NAT holds N is included_in_Seg