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