for n being Nat
for N being non empty Subset of NAT st N c= Segm n holds
min* N <= n - 1