theorem Th2: :: AFINSQ_2:2

for X0 being finite natural-membered set ex n being Nat st X0 c= Segm n