for X being non empty finite Subset of NAT ex n being Element of NAT st X c= (Seg n) \/ {0}